Commit 2023-07-06 15:47 a26c4ef5

View on Github →

feat: in a preconnected space, a (finite) disjoint cover of non-empty open/closed/clopen subsets contains at most one element. (#5677)

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.nonempty_of_nonempty_iUnion

added theorem Set.nonempty_of_nonempty_iUnion_eq_univ

Modified Mathlib/Topology/Connected.lean

added theorem subsingleton_of_disjoint_isClopen

added theorem subsingleton_of_disjoint_isClosed_iUnion_eq_univ

added theorem subsingleton_of_disjoint_isOpen_iUnion_eq_univ