Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_clopen.eq_univ

Modification history

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