English
If each K(n) is Lindelöf, then the accumulate set Accumulate(K,n) is Lindelöf.
Русский
Если каждый K(n) — Линдельёфово, то накопленное множество Accumulate(K,n) тоже Линдельёфово.
LaTeX
$$$\forall n, IsLindelof(K(n)) \Rightarrow IsLindelof(Accumulate(K,n)).$$$
Lean4
/-- A set `s` is Lindelöf if for every open cover of `s`, there exists a countable subcover. -/
theorem isLindelof_of_countable_subcover
(h :
∀ {ι : Type u} (U : ι → Set X),
(∀ i, IsOpen (U i)) → (s ⊆ ⋃ i, U i) → ∃ t : Set ι, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i) :
IsLindelof s := fun f hf hfs ↦ by
contrapose! h
simp only [ClusterPt, not_neBot, ← disjoint_iff, SetCoe.forall', (nhds_basis_opens _).disjoint_iff_left] at h
choose fsub U hU hUf using h
refine ⟨s, U, fun x ↦ (hU x).2, fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, (hU _).1⟩, ?_⟩
intro t ht h
have uinf := f.sets_of_superset (le_principal_iff.1 fsub) h
have uninf : ⋂ i ∈ t, (U i)ᶜ ∈ f := (countable_bInter_mem ht).mpr (fun _ _ ↦ hUf _)
rw [← compl_iUnion₂] at uninf
have uninf := compl_notMem uninf
simp only [compl_compl] at uninf
contradiction
