Commit 2026-09-02 00:40 4c2e36ef

View on Github →

chore(Topology/Separation): generalize theorems on IndiscreteTopology (#42317) Generalize some theorems on IndiscreteTopology from EMetricSpace to T0Space. Also move subsingleton_iff_discrete_and_indiscrete to an earlier file because it has an easier proof.

Estimated changes

Modified Mathlib/Topology/EMetricSpace/Basic.lean

deleted theorem EMetric.nontrivial_iff_nontrivialTopology

deleted theorem EMetric.subsingleton_iff_indiscreteTopology

Modified Mathlib/Topology/Separation/Basic.lean

added theorem nontrivial_iff_nontrivialTopology

added theorem subsingleton_iff_discrete_and_indiscrete

added theorem subsingleton_iff_indiscreteTopology

Modified Mathlib/Topology/Separation/Connected.lean

deleted theorem subsingleton_iff_discrete_and_indiscrete