Theorem OpenPartialHomeomorph.contMDiffWithinAt_writtenInExtend_iff

Modification history

2026-03-19 14:41
Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
feat: smoothness on a set can be checked in extended charts (#36816) …
Added OpenPartialHomeomorph.contMDiffWithinAt_writtenInExtend_iffView on Github →