Theorem Set.nonempty_of_nonempty_iUnion_eq_univ

Modification history

2023-07-06 15:47
Mathlib/Data/Set/Lattice.lean
feat: in a preconnected space, a (finite) disjoint cover of non-empty open/closed/clopen subsets contains at most one element. (#5677)
Added Set.nonempty_of_nonempty_iUnion_eq_univView on Github →