Commit 2026-01-08 19:45 44d88035

View on Github →

feat: uniqueness API for implicit function of IsContDiffImplicitAt (#31988)

Estimated changes

Modified Mathlib/Analysis/Calculus/Implicit.lean

added theorem ImplicitFunctionData.eventuallyEq_implicitFunction

added theorem ImplicitFunctionData.implicitFunction_apply

Modified Mathlib/Analysis/Calculus/ImplicitContDiff.lean

added theorem IsContDiffImplicitAt.eventually_implicitFunction_apply_eq

added theorem IsContDiffImplicitAt.implicitFunctionData_leftFun_apply

deleted theorem IsContDiffImplicitAt.implicitFunctionData_leftFun_pt

added theorem IsContDiffImplicitAt.implicitFunctionData_pt

added theorem IsContDiffImplicitAt.implicitFunctionData_rightFun_apply

deleted theorem IsContDiffImplicitAt.implicitFunctionData_rightFun_pt

added theorem IsContDiffImplicitAt.implicitFunction_apply