English
If X has a second-countable topology, is locally compact, and Y is second-countable, then the function space C(X,Y) is separable.
Русский
Если X имеет вторую счетную топологию, локально компактно и Y имеет вторую счетность, то пространство функций C(X,Y) сепарабельно.
LaTeX
$$$\\text{SeparableSpace } C(X,Y)$$$
Lean4
instance instSecondCountableTopology [SecondCountableTopology X] [LocallyCompactSpace X] [SecondCountableTopology Y] :
SecondCountableTopology C(X, Y) := by
apply secondCountableTopology
have (U : countableBasis X) : LocallyCompactSpace U.1 := (isOpen_of_mem_countableBasis U.2).locallyCompactSpace
set K := fun U : countableBasis X ↦ CompactExhaustion.choice U.1
use ⋃ U : countableBasis X, Set.range fun n ↦ K U n
refine ⟨countable_iUnion fun _ ↦ countable_range _, ?_, ?_⟩
· simp only [mem_iUnion, mem_range]
rintro K ⟨U, n, rfl⟩
exact ((K U).isCompact _).image continuous_subtype_val
· intro f V hVo x hxV
obtain ⟨U, hU, hxU, hUV⟩ : ∃ U ∈ countableBasis X, x ∈ U ∧ U ⊆ f ⁻¹' V :=
by
rw [← (isBasis_countableBasis _).mem_nhds_iff]
exact (hVo.preimage (map_continuous f)).mem_nhds hxV
lift x to U using hxU
lift U to countableBasis X using hU
rcases (K U).exists_mem_nhds x with ⟨n, hn⟩
refine ⟨K U n, mem_iUnion.2 ⟨U, mem_range_self _⟩, ?_, ?_⟩
· rw [← map_nhds_subtype_coe_eq_nhds x.2]
exacts [image_mem_map hn, (isOpen_of_mem_countableBasis U.2).mem_nhds x.2]
· rw [mapsTo_image_iff]
exact fun y _ ↦ hUV y.2
