English
In a second-countable space, for any f and s, a countable subfamily of nhdsWithin exists that covers s.
Русский
Во втором счетном пространстве существует счётное подпокрытие внутри подмножества s.
LaTeX
$$$[SecondCountableTopology\ α] {f : α \to Set α} {s : Set α} (hf : \forall x\, x\in s, f(x) ∈ nhdsWithin x s) : \exists t \subseteq s, t.Countable ∧ s \subseteq ⋃ x∈t, f(x)$$$
Lean4
theorem countable_cover_nhdsWithin [SecondCountableTopology α] {f : α → Set α} {s : Set α}
(hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x :=
by
have : ∀ x : s, (↑) ⁻¹' f x ∈ 𝓝 x := fun x => preimage_coe_mem_nhds_subtype.2 (hf x x.2)
rcases countable_cover_nhds this with ⟨t, htc, htU⟩
refine ⟨(↑) '' t, Subtype.coe_image_subset _ _, htc.image _, fun x hx => ?_⟩
simp only [biUnion_image, eq_univ_iff_forall, ← preimage_iUnion, mem_preimage] at htU ⊢
exact htU ⟨x, hx⟩
