English
In a second-countable space, for any function f sending each point to a neighborhood of that point, there exists a countable set of centers whose neighborhoods cover the space.
Русский
В пространстве со второй счетностью для любой функции f, отправляющей точку в окрестность этой точки, существует счётное множество центров, чьи окрестности покрывают пространство.
LaTeX
$$$[SecondCountableTopology\ α] {f : α \to Set α} (hf : \forall x, f(x) \in 𝓝 x) : \exists s, s.Countable ∧ ⋃ x∈s, f(x) = univ$$$
Lean4
/-- In a topological space with second countable 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 [SecondCountableTopology α] {f : α → Set α} (hf : ∀ x, f x ∈ 𝓝 x) :
∃ s : Set α, s.Countable ∧ ⋃ x ∈ s, f x = univ :=
by
rcases isOpen_iUnion_countable (fun x => interior (f x)) fun x => isOpen_interior with ⟨s, hsc, hsU⟩
suffices ⋃ x ∈ s, interior (f x) = univ from
⟨s, hsc, flip eq_univ_of_subset this <| iUnion₂_mono fun _ _ => interior_subset⟩
simp only [hsU, eq_univ_iff_forall, mem_iUnion]
exact fun x => ⟨x, mem_interior_iff_mem_nhds.2 (hf x)⟩
