Theorem subsingleton_iff_discrete_and_indiscrete

Modification history

2026-09-02 00:40
Mathlib/Topology/Separation/Basic.lean
chore(Topology/Separation): generalize theorems on `IndiscreteTopology` (#42317) …
Modified subsingleton_iff_discrete_and_indiscreteView on Github →
2026-05-19 19:46
Mathlib/Topology/Separation/Connected.lean
feat: add `IndiscreteTopology` instances (#38097)
Added subsingleton_iff_discrete_and_indiscreteView on Github →