Theorem TopologicalSpace.Opens.chartAt_eq

Modification history

2026-01-15 09:15
Mathlib/Geometry/Manifold/ChartedSpace.lean
refactor(Geometry/Manifold): split long file ChartedSpace.lean (#33896) …
Modified TopologicalSpace.Opens.chartAt_eqView on Github →
2025-12-12 15:51
Mathlib/Geometry/Manifold/ChartedSpace.lean
feat(Geometry/Manifold): interior and boundary of open subsets of manifolds (#32759) …
Added TopologicalSpace.Opens.chartAt_eqView on Github →