Theorem Filter.EventuallyEq.mdifferentiablefWithinAt_iff

Modification history

2025-07-04 16:11
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
feat: missing congruence lemmas for mdifferentiability (#26709) …
Added Filter.EventuallyEq.mdifferentiablefWithinAt_iffView on Github →