countable_of_isOpen — Mathlib

English

In a separable space, a subfamily of pairwise disjoint open sets is countable.

Русский

В сепарабельном пространстве подсемейство попарно непересекающихся открытых множеств так же счётно.

LaTeX

$$$\forall a\subseteq ι,\ (a\mathbin{.}PairwiseDisjoint\ s) \rightarrow a.Countable$ (assuming separability of the ambient space).$$

Lean4

/-- In a separable space, a family of nonempty disjoint open sets is countable. -/
theorem _root_.Set.PairwiseDisjoint.countable_of_isOpen [SeparableSpace α] {ι : Type*} {s : ι → Set α} {a : Set ι}
    (h : a.PairwiseDisjoint s) (ho : ∀ i ∈ a, IsOpen (s i)) (hne : ∀ i ∈ a, (s i).Nonempty) : a.Countable :=
  (h.subtype _ _).countable_of_isOpen_disjoint (Subtype.forall.2 ho) (Subtype.forall.2 hne)

Похожие утверждения