Theorem nonempty_of_chartedSpace

Modification history

2025-02-11 13:31

Mathlib/Geometry/Manifold/ChartedSpace.lean

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

Added nonempty_of_chartedSpace View on Github →