Theorem EMetric.t4Space

Modification history

2026-02-01 00:20

Mathlib/Topology/EMetricSpace/Paracompact.lean

refactor(EMetricSpace): rename `EMetric.ball` -> `Metric.eball` (#34379) …

Deleted EMetric.t4Space View on Github →

2023-09-12 17:41

Mathlib/Topology/EMetricSpace/Paracompact.lean

refactor: split `NormalSpace` into `NormalSpace` and `T4Space` (#7072) …

Added EMetric.t4Space View on Github →