countable_of_nonempty_interior — Mathlib

English

In a separable space, a family of disjoint sets with nonempty interiors is countable.

Русский

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

LaTeX

$$$\forall a\subseteq ι,\ (\forall i\in a, (\operatorname{interior}(s_i)).Nonempty) \rightarrow a.Countable$$$

Lean4

/-- In a separable space, a family of disjoint sets with nonempty interiors is countable. -/
theorem _root_.Set.PairwiseDisjoint.countable_of_nonempty_interior [SeparableSpace α] {ι : Type*} {s : ι → Set α}
    {a : Set ι} (h : a.PairwiseDisjoint s) (ha : ∀ i ∈ a, (interior (s i)).Nonempty) : a.Countable :=
  (h.mono fun _ => interior_subset).countable_of_isOpen (fun _ _ => isOpen_interior) ha

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