English
If s is countable and each f_i is Lindelöf, then the union ⋃_{i∈s} f_i is Lindelöf.
Русский
Если s счётно и для каждого i∈s f_i — Линдельёфово, тогда ⋃_{i∈s} f_i Линдельёфово.
LaTeX
$$$s\text{ countable} \to (\forall i\in s, IsLindelof(f_i)) \to IsLindelof(\bigcup_{i\in s} f_i).$$$
Lean4
theorem isLindelof_biUnion {s : Set ι} {f : ι → Set X} (hs : s.Countable) (hf : ∀ i ∈ s, IsLindelof (f i)) :
IsLindelof (⋃ i ∈ s, f i) := by
apply isLindelof_of_countable_subcover
intro i U hU hUcover
have hiU : ∀ i ∈ s, f i ⊆ ⋃ i, U i := fun _ is ↦ _root_.subset_trans (subset_biUnion_of_mem is) hUcover
have iSets := fun i is ↦ (hf i is).elim_countable_subcover U hU (hiU i is)
choose! r hr using iSets
use ⋃ i ∈ s, r i
constructor
· refine (Countable.biUnion_iff hs).mpr ?h.left.a
exact fun s hs ↦ (hr s hs).1
· refine iUnion₂_subset ?h.right.h
intro i is
simp only [mem_iUnion, exists_prop, iUnion_exists, biUnion_and']
intro x hx
exact mem_biUnion is ((hr i is).2 hx)
