Gδ sets and metrizable spaces

Main results

We prove that metrizable spaces are T6. We prove that the continuity set of a function from a topological space to a metrizable space is a Gδ set.

@[instance 100]

instance instNormalSpaceOfPseudoMetrizableSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] : NormalSpace X

@[instance 500]

instance instPerfectlyNormalSpaceOfPseudoMetrizableSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] : PerfectlyNormalSpace X

@[instance 100]

instance instT4SpaceOfMetrizableSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] : T4Space X

@[instance 500]

instance instT6SpaceOfMetrizableSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] : T6Space X

theorem IsGδ.setOf_continuousAt {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] [TopologicalSpace.PseudoMetrizableSpace Y] (f : X → Y) : IsGδ {x : X | ContinuousAt f x}