Mathlib Changelog
v4
Changelog
About
Github
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