English
In a space with sigma-compact topology, if S is closed and for each x ∈ S we have a neighborhood f(x) inside S, then there exists a countable subset T ⊆ S such that S is contained in the union of f(x) for x ∈ T.
Русский
В пространстве с σ-компактной топологией, если S замкнуто, и для каждого x ∈ S даны окрестности f(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` of a closed set `s` to a neighborhood of `x` within `s`, then for some countable set `t ⊆ s`,
the neighborhoods `f x`, `x ∈ t`, cover the whole set `s`. -/
theorem countable_cover_nhdsWithin_of_sigmaCompact {f : X → Set X} {s : Set X} (hs : IsClosed s)
(hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x :=
by
simp only [nhdsWithin, mem_inf_principal] at hf
choose t ht hsub using fun n =>
((isCompact_compactCovering X n).inter_right hs).elim_nhds_subcover _ fun x hx => hf x hx.right
refine
⟨⋃ n, (t n : Set X), iUnion_subset fun n x hx => (ht n x hx).2, countable_iUnion fun n => (t n).countable_toSet,
fun x hx => mem_iUnion₂.2 ?_⟩
rcases exists_mem_compactCovering x with ⟨n, hn⟩
rcases mem_iUnion₂.1 (hsub n ⟨hn, hx⟩) with ⟨y, hyt : y ∈ t n, hyf : x ∈ s → x ∈ f y⟩
exact ⟨y, mem_iUnion.2 ⟨n, hyt⟩, hyf hx⟩
