mathlib3

8deb2a68 - feat(topology/separation): connected sets in a t1 space are infinite (#16584)

feat(topology/separation): connected sets in a t1 space are infinite (#16584) Also rename `eq_univ_of_nonempty_clopen` to `is_clopen.eq_univ`. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>