Mathlib v3 is deprecated. Go to Mathlib v4

Theorem preconnected_space.trivial_of_discrete

Modification history

2022-09-23 17:33
src/topology/separation.lean
feat(topology/separation): connected sets in a t1 space are infinite (#16584) …
Added preconnected_space.trivial_of_discreteView on Github →