Commit 2025-02-11 13:31 c9287802

View on Github →

feat: remove nonemptiness assumption for the sum of manifolds (#21500)

Estimated changes

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

modified theorem ChartedSpace.mem_atlas_sum

added def ChartedSpace.sum_of_nonempty

added theorem isEmpty_of_chartedSpace

added theorem nonempty_of_chartedSpace

added theorem sum_chartAt_inl_apply

added theorem sum_chartAt_inr_apply

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

added theorem contMDiffAt_of_subsingleton

added theorem contMDiffOn_of_subsingleton

added theorem contMDiffWithinAt_of_subsingleton

added theorem contMDiff_of_subsingleton

Modified Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean