Theorem HasMFDerivWithinAt.mono_of_mem

Modification history

2024-11-02 14:17

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

chore: expand `fderiv` API (#18512) …

Deleted HasMFDerivWithinAt.mono_of_mem View on Github →

2023-08-25 14:43

Mathlib/Geometry/Manifold/MFDeriv.lean

chore: remove duplicate lemma HasFDerivWithinAt.nhdsWithin (#6773) …

Added HasMFDerivWithinAt.mono_of_mem View on Github →