English
In a Hereditarily Lindelöf space, any union of open sets has a countable subfamily that covers the same union.
Русский
В пространстве с наследуемой линдельфовостью любая объединение открытых множеств имеет счетное подпокрытие, дающее ту же объединение.
LaTeX
$$$[HereditarilyLindelofSpace X]\\; (U_i)_{i\\in I},\\; (\\forall i, IsOpen(U_i)) \\Rightarrow \\exists t\\subseteq I, t.Countable \\wedge \\bigcup_{i\\in t} U_i = \\bigcup_{i\\in I} U_i.$$$
Lean4
theorem eq_open_union_countable [HereditarilyLindelofSpace X] {ι : Type u} (U : ι → Set X) (h : ∀ i, IsOpen (U i)) :
∃ t : Set ι, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i :=
by
have : IsLindelof (⋃ i, U i) := HereditarilyLindelof_LindelofSets (⋃ i, U i)
rcases isLindelof_iff_countable_subcover.mp this U h (Eq.subset rfl) with ⟨t, ⟨htc, htu⟩⟩
use t, htc
apply eq_of_subset_of_subset (iUnion₂_subset_iUnion (fun i ↦ i ∈ t) fun i ↦ U i) htu
