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
XandYhave second countable topology; Xis 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)
:
ContinuousMap.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)
:
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]
:
Equations
- ⋯ = ⋯
instance
ContinuousMap.instSeparableSpace
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[SecondCountableTopology X]
[LocallyCompactSpace X]
[SecondCountableTopology Y]
:
Equations
- ⋯ = ⋯