Theorem ModelWithCorners.contMDiff

Modification history

2026-06-16 13:03
Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
feat: an explicit criterion for membership in the maximal atlas of a `C^n` manifold (#40632) …
Added ModelWithCorners.contMDiffView on Github →