English
In a separable space, any family of nonempty pairwise disjoint open sets is countable.
Русский
В сепарабельном пространстве любая коллекция непустых попарно непересекающихся открытых множеств счётна.
LaTeX
$$$\operatorname{SeparableSpace}(\alpha) \rightarrow \forall ι, \forall s: ι\to Set(α),\ (\forall i\neq j, s(i) \cap s(j)=\varnothing) \\rightarrow (\forall i, IsOpen(s(i))) \\rightarrow (\forall i, (s(i)).Nonempty) \rightarrow Countable(ι)$$$
Lean4
/-- In a separable space, a family of nonempty disjoint open sets is countable. -/
theorem _root_.Pairwise.countable_of_isOpen_disjoint [SeparableSpace α] {ι : Type*} {s : ι → Set α}
(hd : Pairwise (Disjoint on s)) (ho : ∀ i, IsOpen (s i)) (hne : ∀ i, (s i).Nonempty) : Countable ι :=
by
rcases exists_countable_dense α with ⟨u, u_countable, u_dense⟩
choose f hfu hfs using fun i ↦ u_dense.exists_mem_open (ho i) (hne i)
have f_inj : Injective f := fun i j hij ↦ hd.eq <| not_disjoint_iff.2 ⟨f i, hfs i, hij.symm ▸ hfs j⟩
have := u_countable.to_subtype
exact (f_inj.codRestrict hfu).countable
