English
For every Lindelöf set s and a family of open neighborhoods U(x) of each x∈s, there exists a countable subfamily that still covers s using the neighborhoods U(x).
Русский
Для множества s, Линдельёфового, существует счётное подпокрытие самосогласованной системы окрестностей.
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
theorem elim_nhds_subcover (hs : IsLindelof s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ 𝓝 x) :
∃ t : Set X, t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x :=
by
let ⟨t, ⟨htc, htsub⟩⟩ := hs.elim_nhds_subcover' (fun x _ ↦ U x) hU
refine ⟨↑t, Countable.image htc Subtype.val, ?_⟩
constructor
· intro _
simp only [mem_image, Subtype.exists, exists_and_right, exists_eq_right, forall_exists_index]
tauto
· have : ⋃ x ∈ t, U ↑x = ⋃ x ∈ Subtype.val '' t, U x := biUnion_image.symm
rwa [← this]
