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.