Theorem ChartedSpace.mem_atlas_sum

Modification history

2025-02-11 13:31
Mathlib/Geometry/Manifold/ChartedSpace.lean
feat: remove nonemptiness assumption for the sum of manifolds (#21500)
Modified ChartedSpace.mem_atlas_sumView on Github →
2025-01-11 05:59
Mathlib/Geometry/Manifold/ChartedSpace.lean
feat: disjoint union of charted spaces (#20619) …
Added ChartedSpace.mem_atlas_sumView on Github →