Def ChartedSpace.sum_of_nonempty

Modification history

2026-07-27 17:36
Mathlib/Geometry/Manifold/ChartedSpace.lean
chore(Geometry/Manifold): fix defs with underscores (#42115) …
Deleted ChartedSpace.sum_of_nonemptyView on Github →
2025-02-11 13:31
Mathlib/Geometry/Manifold/ChartedSpace.lean
feat: remove nonemptiness assumption for the sum of manifolds (#21500)
Added ChartedSpace.sum_of_nonemptyView on Github →