Gδ sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define
Gδ sets and prove their basic properties.
Main definitions #
is_Gδ: 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
An open set is a Gδ set.
The union of two Gδ sets is a Gδ set.
The set of points where a function is continuous is a Gδ set.
s is called residual if it includes a countable intersection of dense open sets.
Dense open sets are residual.
Dense Gδ sets are residual.