Documentation

Mathlib.Topology.GDelta.MetrizableSpace

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.

source
@[instance 100]
instance instNormalSpaceOfPseudoMetrizableSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] :
NormalSpace X
source
@[instance 500]
instance instPerfectlyNormalSpaceOfPseudoMetrizableSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] :
PerfectlyNormalSpace X
source
@[instance 100]
instance instT4SpaceOfMetrizableSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] :
T4Space X
source
@[instance 500]
instance instT6SpaceOfMetrizableSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] :
T6Space X
source
theorem IsGδ.setOfPred_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}
source
@[deprecated IsGδ.setOfPred_continuousAt (since := "2026-07-09")]
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}

Alias of IsGδ.setOfPred_continuousAt.