Theorem nontrivial_iff_nontrivialTopology

Modification history

2026-09-02 00:40
Mathlib/Topology/Separation/Basic.lean
chore(Topology/Separation): generalize theorems on `IndiscreteTopology` (#42317) …
Added nontrivial_iff_nontrivialTopologyView on Github →