Theorem EMetric.subsingleton_iff_indiscreteTopology

Modification history

2026-01-28 19:17
Mathlib/Topology/EMetricSpace/Basic.lean
feat: add a typeclass for the indiscrete topology (#29120) …
Added EMetric.subsingleton_iff_indiscreteTopologyView on Github →