Theorem EMetric.nontrivial_iff_nontrivialTopology

Modification history

2026-09-02 00:40
Mathlib/Topology/EMetricSpace/Basic.lean
chore(Topology/Separation): generalize theorems on `IndiscreteTopology` (#42317) …
Deleted EMetric.nontrivial_iff_nontrivialTopologyView on Github →
2026-01-28 19:17
Mathlib/Topology/EMetricSpace/Basic.lean
feat: add a typeclass for the indiscrete topology (#29120) …
Added EMetric.nontrivial_iff_nontrivialTopologyView on Github →