# Documentation

Mathlib.Topology.GDelta

# Gδ sets #

In this file we define Gδ sets and prove their basic properties.

## Main definitions #

• IsGδ: a set s is a Gδ set if it can be represented as an intersection of countably many open sets;

• residual: the σ-filter of residual sets. A set s is 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.

## Tags #

Gδ set, residual set

def IsGδ {α : Type u_1} [] (s : Set α) :

A Gδ set is a countable intersection of open sets.

Instances For
theorem IsOpen.isGδ {α : Type u_1} [] {s : Set α} (h : ) :

An open set is a Gδ set.

@[simp]
theorem isGδ_empty {α : Type u_1} [] :
@[simp]
theorem isGδ_univ {α : Type u_1} [] :
IsGδ Set.univ
theorem isGδ_biInter_of_open {α : Type u_1} {ι : Type u_4} [] {I : Set ι} (hI : ) {f : ιSet α} (hf : ∀ (i : ι), i IIsOpen (f i)) :
IsGδ (⋂ (i : ι) (_ : i I), f i)
theorem isGδ_iInter_of_open {α : Type u_1} {ι : Type u_4} [] [] {f : ιSet α} (hf : ∀ (i : ι), IsOpen (f i)) :
IsGδ (⋂ (i : ι), f i)
theorem isGδ_iInter {α : Type u_1} {ι : Type u_4} [] [] {s : ιSet α} (hs : ∀ (i : ι), IsGδ (s i)) :
IsGδ (⋂ (i : ι), s i)

The intersection of an encodable family of Gδ sets is a Gδ set.

theorem isGδ_biInter {α : Type u_1} {ι : Type u_4} [] {s : Set ι} (hs : ) {t : (i : ι) → i sSet α} (ht : ∀ (i : ι) (hi : i s), IsGδ (t i hi)) :
IsGδ (⋂ (i : ι) (h : i s), t i h)
theorem isGδ_sInter {α : Type u_1} [] {S : Set (Set α)} (h : ∀ (s : Set α), s SIsGδ s) (hS : ) :

A countable intersection of Gδ sets is a Gδ set.

theorem IsGδ.inter {α : Type u_1} [] {s : Set α} {t : Set α} (hs : IsGδ s) (ht : IsGδ t) :
IsGδ (s t)
theorem IsGδ.union {α : Type u_1} [] {s : Set α} {t : Set α} (hs : IsGδ s) (ht : IsGδ t) :
IsGδ (s t)

The union of two Gδ sets is a Gδ set.

theorem isGδ_biUnion {α : Type u_1} {ι : Type u_4} [] {s : Set ι} (hs : ) {f : ιSet α} (h : ∀ (i : ι), i sIsGδ (f i)) :
IsGδ (⋃ (i : ι) (_ : i s), f i)

The union of finitely many Gδ sets is a Gδ set.

theorem IsClosed.isGδ {α : Type u_5} [] {s : Set α} (hs : ) :
theorem isGδ_compl_singleton {α : Type u_1} [] [] (a : α) :
theorem Set.Countable.isGδ_compl {α : Type u_1} [] [] {s : Set α} (hs : ) :
theorem Set.Finite.isGδ_compl {α : Type u_1} [] [] {s : Set α} (hs : ) :
theorem Set.Subsingleton.isGδ_compl {α : Type u_1} [] [] {s : Set α} (hs : ) :
theorem Finset.isGδ_compl {α : Type u_1} [] [] (s : ) :
IsGδ (s)
theorem isGδ_singleton {α : Type u_1} [] [] (a : α) :
IsGδ {a}
theorem Set.Finite.isGδ {α : Type u_1} [] [] {s : Set α} (hs : ) :
theorem isGδ_setOf_continuousAt {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :
IsGδ {x | }

The set of points where a function is continuous is a Gδ set.

def residual (α : Type u_5) [] :

A set s is called residual if it includes a countable intersection of dense open sets.

Instances For
instance countableInterFilter_residual {α : Type u_1} [] :
theorem residual_of_dense_open {α : Type u_1} [] {s : Set α} (ho : ) (hd : ) :
s

Dense open sets are residual.

theorem residual_of_dense_Gδ {α : Type u_1} [] {s : Set α} (ho : IsGδ s) (hd : ) :
s

Dense Gδ sets are residual.

theorem mem_residual_iff {α : Type u_1} [] {s : Set α} :
s S, (∀ (t : Set α), t S) (∀ (t : Set α), t S) ⋂₀ S s

A set is residual iff it includes a countable intersection of dense open sets.