English
In a preconnected space, a finite disjoint open cover by nonempty closed subsets has at most one element.
Русский
В предсвязанном пространстве конечная дизъюнкция непустых закрытых попарно несовпадающих подмножеств имеет не более одного элемента.
LaTeX
$$$[PreconnectedSpace\;\alpha] \; [Finite ι] \; (\forall i, IsClosed (s_i)) \Rightarrow (\bigcup_i s_i = \mathrm{univ}) \Rightarrow \text{Subsingleton } i$$$
Lean4
/-- In a preconnected space, any finite disjoint cover by non-empty closed subsets has at most one
element. -/
theorem 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_of_finite (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
