Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-23 17:33 8deb2a68

View on Github →

feat(topology/separation): connected sets in a t1 space are infinite (#16584) Also rename eq_univ_of_nonempty_clopen to is_clopen.eq_univ.

Estimated changes

added theorem is_clopen.eq_univ