Gδ sets and uniform spaces #
Main results #
We prove that the continuity set of a function from a topological space to a uniform space is a Gδ set.
theorem
IsClosed.isGδ
{X : Type u_3}
[UniformSpace X]
[(uniformity X).IsCountablyGenerated]
{s : Set X}
(hs : IsClosed s)
:
IsGδ s
theorem
IsGδ.setOf_continuousAt
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[UniformSpace Y]
[(uniformity Y).IsCountablyGenerated]
(f : X → Y)
:
IsGδ {x : X | ContinuousAt f x}
The set of points where a function is continuous is a Gδ set.
@[deprecated IsGδ.setOf_continuousAt]
theorem
isGδ_setOf_continuousAt
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[UniformSpace Y]
[(uniformity Y).IsCountablyGenerated]
(f : X → Y)
:
IsGδ {x : X | ContinuousAt f x}
Alias of IsGδ.setOf_continuousAt.
The set of points where a function is continuous is a Gδ set.