Theorem ChartedSpace.isOpen_iff

Modification history

2024-01-16 21:01
Mathlib/Geometry/Manifold/ChartedSpace.lean
feat: subset of a charted space is open iff each image in charts is (#9672) …
Added ChartedSpace.isOpen_iffView on Github →