Theorem sum_chartAt_inr_apply

Modification history

2025-02-25 18:02
Mathlib/Geometry/Manifold/ChartedSpace.lean
chore: add lemmas about charts on disjoint unions to mfld_simps (#22011) …
Modified sum_chartAt_inr_applyView on Github →
2025-02-11 13:31
Mathlib/Geometry/Manifold/ChartedSpace.lean
feat: remove nonemptiness assumption for the sum of manifolds (#21500)
Added sum_chartAt_inr_applyView on Github →