Theorem EMetric.t4Space

Modification history

2023-09-12 17:41
Mathlib/Topology/EMetricSpace/Paracompact.lean
refactor: split `NormalSpace` into `NormalSpace` and `T4Space` (#7072) …
Added EMetric.t4SpaceView on Github →