Def ChartedSpace.of_discreteTopology

Modification history

2026-07-27 17:36
Mathlib/Geometry/Manifold/ChartedSpace.lean
chore(Geometry/Manifold): fix defs with underscores (#42115) …
Deleted ChartedSpace.of_discreteTopologyView on Github →
2025-02-24 09:31
Mathlib/Geometry/Manifold/ChartedSpace.lean
feat: discrete topological spaces are 0-manifolds (#22105) …
Added ChartedSpace.of_discreteTopologyView on Github →