Commit 2025-02-25 18:02 98b31058

View on Github →

chore: add lemmas about charts on disjoint unions to mfld_simps (#22011) These are lemmas about charts on manifolds, hence should also be part of the mfld_simps set.

Estimated changes

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

modified theorem sum_chartAt_inl_apply

modified theorem sum_chartAt_inr_apply

Modified Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean

Modified Mathlib/Topology/PartialHomeomorph.lean