isOpen_sUnion_countable — Mathlib

English

In a second-countable space, given a family of open sets, there exists a countable subfamily whose union equals the union of all sets.

Русский

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

LaTeX

$$$[SecondCountableTopology\ α] \{s : ι \to Set α\} (H : \forall i, IsOpen(s(i))) : \exists T \subseteq ι, T.Countable ∧ ⋃ i∈T, s(i) = ⋃ i, s(i)$$$

Lean4

theorem isOpen_sUnion_countable [SecondCountableTopology α] (S : Set (Set α)) (H : ∀ s ∈ S, IsOpen s) :
    ∃ T : Set (Set α), T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S := by
  simpa only [and_left_comm, sUnion_eq_biUnion] using isOpen_biUnion_countable S id H

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