Second countable topology on C(X, Y)

In this file we prove that C(X, Y) with compact-open topology has second countable topology, if

• both X and Y have second countable topology;
• X is a locally compact space;

theorem ContinuousMap.compactOpen_eq_generateFrom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {S : Set (Set X)} {T : Set (Set Y)} (hS₁ : ∀ K ∈ S, IsCompact K) (hT : TopologicalSpace.IsTopologicalBasis T) (hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ nhds x ∧ Set.MapsTo (⇑f) K V) : compactOpen = TopologicalSpace.generateFrom (Set.image2 (fun (K : Set X) (t : Set (Set Y)) => {f : C(X, Y) | Set.MapsTo (⇑f) K (⋃₀ t)}) S {t : Set (Set Y) | t.Finite ∧ t ⊆ T})

theorem ContinuousMap.secondCountableTopology {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] (hX : ∃ (S : Set (Set X)), S.Countable ∧ (∀ K ∈ S, IsCompact K) ∧ ∀ (f : C(X, Y)) (V : Set Y), IsOpen V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ nhds x ∧ Set.MapsTo (⇑f) K V) : SecondCountableTopology C(X, Y)

A version of instSecondCountableTopology with a technical assumption instead of [SecondCountableTopology X] [LocallyCompactSpace X]. It is here as a reminder of what could be an intermediate goal, if someone tries to weaken the assumptions in the instance (e.g., from [LocallyCompactSpace X] to [LocallyCompactPair X Y] - not sure if it's true).

instance ContinuousMap.instSecondCountableTopology {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] [LocallyCompactSpace X] [SecondCountableTopology Y] : SecondCountableTopology C(X, Y)

instance ContinuousMap.instSeparableSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] [LocallyCompactSpace X] [SecondCountableTopology Y] : TopologicalSpace.SeparableSpace C(X, Y)