English
Let X be a Lindelöf space. For every assignment U of neighborhoods of points, there exists a countable set t of points such that the union of the corresponding neighborhoods U(x) (over x in t) covers X; i.e. ⋃_{x∈t} U(x) = X.
Русский
Пусть X — пространство Линдельфа. Для любой функции U, задающей окрестности каждой точки x, найдется счетное подмножество t ⊆ X such that ⋃_{x∈t} U(x) покрывает X (⋃_{x∈t} U(x) = X).
LaTeX
$$$\forall X\,[{\\text{LindelofSpace } X}]\, (U:X \to P(X))\ (hU: \forall x, U(x) \in \mathcal N(x))\Rightarrow\exists t\subseteq X,\ t.Countable \land \bigcup_{x \in t} U(x) = univ$$$
Lean4
theorem elim_nhds_subcover [LindelofSpace X] (U : X → Set X) (hU : ∀ x, U x ∈ 𝓝 x) :
∃ t : Set X, t.Countable ∧ ⋃ x ∈ t, U x = univ :=
by
obtain ⟨t, tc, -, s⟩ := IsLindelof.elim_nhds_subcover isLindelof_univ U fun x _ => hU x
use t, tc
apply top_unique s
