Theorem ChartedSpace.sum_chartAt_inr

Modification history

2025-01-11 05:59
Mathlib/Geometry/Manifold/ChartedSpace.lean
feat: disjoint union of charted spaces (#20619) …
Added ChartedSpace.sum_chartAt_inrView on Github →