English
Let hs be Lindelöf and U a family of sets with U(x) a neighborhood basis at x for each x∈s. Then there exists a countable subfamily of s that covers s by U.
Русский
Пусть hs — Линдельёфово множество, а U—семейство, где для каждого x∈s множество U(x) образует окрестность x. Тогда существует счётное подпокрытие.
LaTeX
$$$IsLindelof(s) \to (U: X \to Set X) \to (\forall x\in s, U(x) \in \mathcal{N}(x)) \to \exists t\subseteq s, t.Countable \land s \subseteq \bigcup_{x\in t} U(x).$$$
Lean4
/-- For every nonempty open cover of a Lindelöf set, there exists a subcover indexed by ℕ. -/
theorem indexed_countable_subcover {ι : Type v} [Nonempty ι] (hs : IsLindelof s) (U : ι → Set X)
(hUo : ∀ i, IsOpen (U i)) (hsU : s ⊆ ⋃ i, U i) : ∃ f : ℕ → ι, s ⊆ ⋃ n, U (f n) :=
by
obtain ⟨c, ⟨c_count, c_cov⟩⟩ := hs.elim_countable_subcover U hUo hsU
rcases c.eq_empty_or_nonempty with rfl | c_nonempty
· simp only [mem_empty_iff_false, iUnion_of_empty, iUnion_empty] at c_cov
simp only [subset_eq_empty c_cov rfl, empty_subset, exists_const]
obtain ⟨f, f_surj⟩ := (Set.countable_iff_exists_surjective c_nonempty).mp c_count
refine ⟨fun x ↦ f x, c_cov.trans <| iUnion₂_subset_iff.mpr (?_ : ∀ i ∈ c, U i ⊆ ⋃ n, U (f n))⟩
intro x hx
obtain ⟨n, hn⟩ := f_surj ⟨x, hx⟩
exact subset_iUnion_of_subset n <| subset_of_eq (by rw [hn])
