English
In a preconnected space, a pairwise disjoint family of nonempty open sets whose union is the whole space has at most one index.
Русский
В предсвязанном пространстве, попарно непересекающееся семейство непустых открытых множеств, чье объединение даёт всё пространство, содержит по существу один индекс.
LaTeX
$$$[PreconnectedSpace\;\alpha] \; (\forall i, IsOpen (s_i)) \Rightarrow (\bigcup_i s_i = \mathrm{univ}) \Rightarrow \text{Subsingleton } i$$$
Lean4
/-- In a preconnected space, any disjoint cover by non-empty open subsets has at most one
element. -/
theorem 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
