Theorem ImplicitFunctionData.contDiffAt_implicitFunction

Modification history

2026-04-17 18:09

Mathlib/Analysis/Calculus/ImplicitContDiff.lean

feat(Analysis/Calculus/ContDiff): add notation `ℕ∞ω` for `WithTop ℕ∞` (#34649) …

Modified ImplicitFunctionData.contDiffAt_implicitFunction View on Github →

2026-03-20 16:11

Mathlib/Analysis/Calculus/ImplicitContDiff.lean

feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfProdDomain (#26985) …

Added ImplicitFunctionData.contDiffAt_implicitFunction View on Github →