Commit 2026-03-20 16:11 ef7aa4b6

View on Github →

feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfProdDomain (#26985) This PR continues the work from #16743. Original PR: https://github.com/leanprover-community/mathlib4/pull/16743

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/Implicit.lean

added theorem ImplicitFunctionData.hasStrictFDerivAt_implicitFunction

added theorem ImplicitFunctionData.implicitFunction_def

deleted theorem ImplicitFunctionData.implicitFunction_hasStrictFDerivAt

added theorem ImplicitFunctionData.leftFun_eq_iff_implicitFunction

added theorem ImplicitFunctionData.leftFun_implicitFunction

added theorem ImplicitFunctionData.leftFun_implicitFunction_eq_leftFun

deleted theorem ImplicitFunctionData.left_map_implicitFunction

modified theorem ImplicitFunctionData.prodFun_apply

added theorem ImplicitFunctionData.prodFun_implicitFunction

deleted theorem ImplicitFunctionData.prod_map_implicitFunction

added theorem ImplicitFunctionData.rightFun_implicitFunction

added theorem ImplicitFunctionData.rightFun_implicitFunction_eq_rightFun

deleted theorem ImplicitFunctionData.right_map_implicitFunction

modified theorem ImplicitFunctionData.toOpenPartialHomeomorph_coe

Modified Mathlib/Analysis/Calculus/ImplicitContDiff.lean

added theorem ContDiffAt.contDiffAt_implicitFunction

added theorem ContDiffAt.eventually_apply_eq_iff_implicitFunction

added theorem ContDiffAt.eventually_apply_implicitFunction

added theorem ContDiffAt.hasStrictFDerivAt_implicitFunction

added theorem ContDiffAt.implicitFunction_apply_self

added theorem ContDiffAt.implicitFunction_def

added theorem ImplicitFunctionData.contDiffAt_implicitFunction

deleted theorem ImplicitFunctionData.contDiff_implicitFunction

deleted theorem IsContDiffImplicitAt.apply_implicitFunction

deleted theorem IsContDiffImplicitAt.comp_implicitFunctionAux_eq_snd

deleted theorem IsContDiffImplicitAt.contDiffAt_implicitFunction

deleted theorem IsContDiffImplicitAt.eventually_implicitFunction_apply_eq

deleted theorem IsContDiffImplicitAt.implicitFunctionAux_fst

deleted def IsContDiffImplicitAt.implicitFunctionData

deleted theorem IsContDiffImplicitAt.implicitFunctionData_leftFun_apply

deleted theorem IsContDiffImplicitAt.implicitFunctionData_leftFun_pt

deleted theorem IsContDiffImplicitAt.implicitFunctionData_pt

deleted theorem IsContDiffImplicitAt.implicitFunctionData_rightFun_apply

deleted theorem IsContDiffImplicitAt.implicitFunctionData_rightFun_pt

deleted theorem IsContDiffImplicitAt.implicitFunction_apply

deleted theorem IsContDiffImplicitAt.implicitFunction_def

deleted theorem IsContDiffImplicitAt.one_le

modified structure IsContDiffImplicitAt

Created Mathlib/Analysis/Calculus/ImplicitFunction/ProdDomain.lean

added theorem HasStrictFDerivAt.eventually_apply_eq_iff_implicitFunctionOfProdDomain

added theorem HasStrictFDerivAt.eventually_apply_implicitFunctionOfProdDomain

added theorem HasStrictFDerivAt.hasStrictFDerivAt_implicitFunctionOfProdDomain

added def HasStrictFDerivAt.implicitFunctionDataOfProdDomain

added theorem HasStrictFDerivAt.implicitFunctionOfProdDomain_def

added theorem HasStrictFDerivAt.leftFun_implicitFunctionDataOfProdDomain

added theorem HasStrictFDerivAt.pt_implicitFunctionDataOfProdDomain

added theorem HasStrictFDerivAt.rightFun_implicitFunctionDataOfProdDomain

added theorem HasStrictFDerivAt.tendsto_implicitFunctionOfProdDomain