English
For every open cover of a Lindelöf set s, there exists a countable subcover.
Русский
Для любого открытого покрытия множества Линдельёфа s существует счётное подпокрытие.
LaTeX
$$$IsLindelof(s) \to \forall(U: \iota \to Set X),\ (\forall i, IsOpen(U(i))) \to (s \subseteq \bigcup_i U(i)) \to \exists r \subseteq \iota, r\text{ Countable} \land (s \subseteq \bigcup_{i\in r} U(i)).$$$
Lean4
/-- For every open cover of a Lindelöf set, there exists a countable subcover. -/
theorem elim_countable_subcover {ι : Type v} (hs : IsLindelof s) (U : ι → Set X) (hUo : ∀ i, IsOpen (U i))
(hsU : s ⊆ ⋃ i, U i) : ∃ r : Set ι, r.Countable ∧ (s ⊆ ⋃ i ∈ r, U i) :=
by
have hmono :
∀ ⦃s t : Set X⦄,
s ⊆ t → (∃ r : Set ι, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → (∃ r : Set ι, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) :=
by
intro _ _ hst ⟨r, ⟨hrcountable, hsub⟩⟩
exact ⟨r, hrcountable, Subset.trans hst hsub⟩
have hcountable_union :
∀ (S : Set (Set X)),
S.Countable →
(∀ s ∈ S, ∃ r : Set ι, r.Countable ∧ (s ⊆ ⋃ i ∈ r, U i)) → ∃ r : Set ι, r.Countable ∧ (⋃₀ S ⊆ ⋃ i ∈ r, U i) :=
by
intro S hS hsr
choose! r hr using hsr
refine ⟨⋃ s ∈ S, r s, hS.biUnion_iff.mpr (fun s hs ↦ (hr s hs).1), ?_⟩
refine sUnion_subset ?h.right.h
simp only [mem_iUnion, exists_prop, iUnion_exists, biUnion_and']
exact fun i is x hx ↦ mem_biUnion is ((hr i is).2 hx)
have h_nhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ r : Set ι, r.Countable ∧ (t ⊆ ⋃ i ∈ r, U i) :=
by
intro x hx
let ⟨i, hi⟩ := mem_iUnion.1 (hsU hx)
refine ⟨U i, mem_nhdsWithin_of_mem_nhds ((hUo i).mem_nhds hi), { i }, by simp, ?_⟩
simp only [mem_singleton_iff, iUnion_iUnion_eq_left]
exact Subset.refl _
exact hs.induction_on hmono hcountable_union h_nhds
