English
If Y has a second-countable topology and X satisfies a base of compact sets giving a suitable pullback condition, then the function space C(X,Y) carries the second-countable topology (via the compact-open topology generated from a countable basis).
Русский
Если Y имеет вторую счетную топологию и X удовлетворяет условию базиса компактов, дающему подходящую оценку вытягивания, то пространство функций C(X,Y) несет вторую счетную топологию (через компактно-открытую топологию).
LaTeX
$$$SecondCountableTopology\\,C(X,Y)$ при условиях на X и Y.$$
Lean4
theorem compactOpen_eq_generateFrom {S : Set (Set X)} {T : Set (Set Y)} (hS₁ : ∀ K ∈ S, IsCompact K)
(hT : IsTopologicalBasis T) (hS₂ : ∀ f : C(X, Y), ∀ x, ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo f K V) :
compactOpen =
.generateFrom (.image2 (fun K t ↦ {f : C(X, Y) | MapsTo f K (⋃₀ t)}) S {t : Set (Set Y) | t.Finite ∧ t ⊆ T}) :=
by
apply le_antisymm
· apply_rules [generateFrom_anti, image2_subset_iff.mpr]
intro K hK t ht
exact mem_image2_of_mem (hS₁ K hK) (isOpen_sUnion fun _ h ↦ hT.isOpen <| ht.2 h)
· refine le_of_nhds_le_nhds fun f ↦ ?_
simp only [nhds_compactOpen, le_iInf_iff, le_principal_iff]
intro K (hK : IsCompact K) U (hU : IsOpen U) hfKU
simp only [TopologicalSpace.nhds_generateFrom]
obtain ⟨t, htT, htf, hTU, hKT⟩ : ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ f '' K ⊆ ⋃₀ t :=
by
rw [hT.open_eq_sUnion' hU, mapsTo_iff_image_subset, sUnion_eq_biUnion] at hfKU
obtain ⟨t, ht, hfin, htK⟩ :=
(hK.image (map_continuous f)).elim_finite_subcover_image (fun V hV ↦ hT.isOpen hV.1) hfKU
refine ⟨t, fun _ h ↦ (ht h).1, hfin, fun _ h ↦ (ht h).2, ?_⟩
rwa [sUnion_eq_biUnion]
rw [image_subset_iff] at hKT
obtain ⟨s, hsS, hsf, hKs, hst⟩ : ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo f (⋃₀ s) (⋃₀ t) :=
by
have : ∀ x ∈ K, ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo f L (⋃₀ t) :=
by
intro x hx
rcases hKT hx with ⟨V, hVt, hxV⟩
rcases hS₂ f x V (htT hVt) hxV with ⟨L, hLS, hLx, hLV⟩
exact ⟨L, hLS, hLx, hLV.mono_right <| subset_sUnion_of_mem hVt⟩
choose! L hLS hLmem hLt using this
rcases hK.elim_nhds_subcover L hLmem with ⟨s, hsK, hs⟩
refine
⟨L '' s, image_subset_iff.2 fun x hx ↦ hLS x <| hsK x hx, s.finite_toSet.image _, by rwa [sUnion_image], ?_⟩
rw [mapsTo_sUnion, forall_mem_image]
exact fun x hx ↦ hLt x <| hsK x hx
have hsub : (⋂ L ∈ s, {g : C(X, Y) | MapsTo g L (⋃₀ t)}) ⊆ {g | MapsTo g K U} :=
by
simp only [← setOf_forall, ← mapsTo_iUnion, ← sUnion_eq_biUnion]
exact fun g hg ↦ hg.mono hKs (sUnion_subset hTU)
refine mem_of_superset ((biInter_mem hsf).2 fun L hL ↦ ?_) hsub
refine mem_iInf_of_mem _ <| mem_iInf_of_mem ?_ <| mem_principal_self _
exact ⟨hst.mono_left (subset_sUnion_of_mem hL), mem_image2_of_mem (hsS hL) ⟨htf, htT⟩⟩
