Gδ sets #
In this file we define
Gδ sets and prove their basic properties.
Main definitions #
IsGδ: a set
Gδset if it can be represented as an intersection of countably many open sets;
residual: the σ-filter of residual sets. A set
sis called residual if it includes a countable intersection of dense open sets.
Main results #
We prove that finite or countable intersections of Gδ sets is a Gδ set. We also prove that the continuity set of a function from a topological space to an (e)metric space is a Gδ set.
Gδ set, residual set