Theorem ContMDiffWithinAt.insert

Modification history

2024-11-06 07:58

Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

feat: expand API of `ContMDiff` and `MFDeriv` (#18623) …

Deleted ContMDiffWithinAt.insert View on Github →

2023-11-30 19:19

Mathlib/Geometry/Manifold/ContMDiff.lean

chore: split Geometry/Manifold/ContMDiff (#8726) …

Modified ContMDiffWithinAt.insert View on Github →

2023-07-26 08:17

Mathlib/Geometry/Manifold/ContMDiff.lean

chore(*): add `protected` to `*.insert` theorems (#6142) …

Added ContMDiffWithinAt.insert View on Github →