English
In a sigma-compact space, given f: X → Set X and s ⊆ X, if every x ∈ s has f(x) ∈ nhdsWithin x s, then there exists a countable subset t ⊆ s with s ⊆ ⋃_{x∈t} f(x).
Русский
В σ-компактном пространстве, для отображения f и множества s ⊆ X, если для каждого x ∈ s выполнено f(x) ∈ nhdsWithin x s, то найдётся счетное подмножество t ⊆ s такое, что s ⊆ ⋃_{x∈t} f(x).
LaTeX
$$$$\exists t \subseteq s,\ t.Countable \land s \subseteq \bigcup_{x\in t} f(x).$$$$
Lean4
/-- In a topological space with sigma compact topology, if `f` is a function that sends each
point `x` to a neighborhood of `x`, then for some countable set `s`, the neighborhoods `f x`,
`x ∈ s`, cover the whole space. -/
theorem countable_cover_nhds_of_sigmaCompact {f : X → Set X} (hf : ∀ x, f x ∈ 𝓝 x) :
∃ s : Set X, s.Countable ∧ ⋃ x ∈ s, f x = univ :=
by
simp only [← nhdsWithin_univ] at hf
rcases countable_cover_nhdsWithin_of_sigmaCompact isClosed_univ fun x _ => hf x with ⟨s, -, hsc, hsU⟩
exact ⟨s, hsc, univ_subset_iff.1 hsU⟩
