Theorem iUnion_source_chartAt

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 iUnion_source_chartAtView on Github →