feat: in a preconnected space, a (finite) disjoint cover of non-empty…

… open/closed/clopen subsets contains at most one element. (#5677)

Mathlib/Data/Set/Lattice.lean

@@ -273,6 +273,15 @@ theorem nonempty_of_union_eq_top_of_nonempty {ι : Type _} (t : Set ι) (s : ι
   exact ⟨x, m⟩
 #align set.nonempty_of_union_eq_top_of_nonempty Set.nonempty_of_union_eq_top_of_nonempty
 
+theorem nonempty_of_nonempty_iUnion
+    {s : ι → Set α} (h_Union : (⋃ i, s i).Nonempty) : Nonempty ι := by
+  obtain ⟨x, hx⟩ := h_Union
+  exact ⟨Classical.choose $ mem_iUnion.mp hx⟩
+
+theorem nonempty_of_nonempty_iUnion_eq_univ
+    {s : ι → Set α} [Nonempty α] (h_Union : ⋃ i, s i = univ) : Nonempty ι :=
+  nonempty_of_nonempty_iUnion (s := s) (by simpa only [h_Union] using univ_nonempty)
+
 theorem setOf_exists (p : ι → β → Prop) : { x | ∃ i, p i x } = ⋃ i, { x | p i x } :=
   ext fun _ => mem_iUnion.symm
 #align set.set_of_exists Set.setOf_exists

Mathlib/Topology/Connected.lean

@@ -863,6 +863,53 @@ theorem IsClopen.eq_univ [PreconnectedSpace α] {s : Set α} (h' : IsClopen s) (
   (isClopen_iff.mp h').resolve_left h.ne_empty
 #align is_clopen.eq_univ IsClopen.eq_univ
 
+section disjoint_subsets
+
+variable [PreconnectedSpace α]
+  {s : ι → Set α} (h_nonempty : ∀ i, (s i).Nonempty) (h_disj : Pairwise (Disjoint on s))
+
+/-- In a preconnected space, any disjoint family of non-empty clopen subsets has at most one
+element. -/
+lemma subsingleton_of_disjoint_isClopen
+    (h_clopen : ∀ i, IsClopen (s i)) :
+    Subsingleton ι := by
+  replace h_nonempty : ∀ i, s i ≠ ∅ := by intro i; rw [← nonempty_iff_ne_empty]; exact h_nonempty i
+  rw [← not_nontrivial_iff_subsingleton]
+  by_contra contra
+  obtain ⟨i, j, h_ne⟩ := contra
+  replace h_ne : s i ∩ s j = ∅ := by
+    simpa only [← bot_eq_empty, eq_bot_iff, ← inf_eq_inter, ← disjoint_iff_inf_le] using h_disj h_ne
+  cases' isClopen_iff.mp (h_clopen i) with hi hi
+  · exact h_nonempty i hi
+  · rw [hi, univ_inter] at h_ne
+    exact h_nonempty j h_ne
+
+/-- In a preconnected space, any disjoint cover by non-empty open subsets has at most one
+element. -/
+lemma subsingleton_of_disjoint_isOpen_iUnion_eq_univ
+    (h_open : ∀ i, IsOpen (s i)) (h_Union : ⋃ i, s i = univ) :
+    Subsingleton ι := by
+  refine' subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨h_open i, _⟩)
+  rw [← isOpen_compl_iff, compl_eq_univ_diff, ← h_Union, iUnion_diff]
+  refine' isOpen_iUnion (fun j ↦ _)
+  rcases eq_or_ne i j with rfl | h_ne
+  · simp
+  · simpa only [(h_disj h_ne.symm).sdiff_eq_left] using h_open j
+
+/-- In a preconnected space, any finite disjoint cover by non-empty closed subsets has at most one
+element. -/
+lemma subsingleton_of_disjoint_isClosed_iUnion_eq_univ [Finite ι]
+    (h_closed : ∀ i, IsClosed (s i)) (h_Union : ⋃ i, s i = univ) :
+    Subsingleton ι := by
+  refine' subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨_, h_closed i⟩)
+  rw [← isClosed_compl_iff, compl_eq_univ_diff, ← h_Union, iUnion_diff]
+  refine' isClosed_iUnion (fun j ↦ _)
+  rcases eq_or_ne i j with rfl | h_ne
+  · simp
+  · simpa only [(h_disj h_ne.symm).sdiff_eq_left] using h_closed j
+
+end disjoint_subsets
+
 theorem frontier_eq_empty_iff [PreconnectedSpace α] {s : Set α} :
     frontier s = ∅ ↔ s = ∅ ∨ s = univ :=
   isClopen_iff_frontier_eq_empty.symm.trans isClopen_iff