Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_preconnected.infinite_of_nontrivial

Modification history

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