English
Given a Lindelöf set s and a family U of sets indexed by s, with U(x) open around each x∈s in a neighborhood sense, there exists a countable subset t of s such that s is contained in the union over x∈t of U(x).
Русский
Пусть s — множество Линдельёфа, и задана семейство U, индексированное элементами s, такое что вокруг каждого x∈s существует набор U(x) с указанной свойством. Тогда существует счётное подмножество t⊆s такое, что s ⊆ ⋃_{x∈t} U(x).
LaTeX
$$$\exists t \subseteq s,\ t.Countable \land s \subseteq \bigcup_{x\in t} U(x).$$$
Lean4
theorem elim_nhds_subcover' (hs : IsLindelof s) (U : ∀ x ∈ s, Set X) (hU : ∀ x (hx : x ∈ s), U x ‹x ∈ s› ∈ 𝓝 x) :
∃ t : Set s, t.Countable ∧ s ⊆ ⋃ x ∈ t, U (x : s) x.2 :=
by
have :=
hs.elim_countable_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior) fun x hx ↦
mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩
rcases this with ⟨r, ⟨hr, hs⟩⟩
use r, hr
apply Subset.trans hs
apply iUnion₂_subset
intro i hi
apply Subset.trans interior_subset
exact subset_iUnion_of_subset i (subset_iUnion_of_subset hi (Subset.refl _))
