mathlib documentation

topology.G_delta

`Gδ` sets

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

Main definitions

is_Gδ: 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 dense Gδ set. In a Baire space (e.g., in a complete (e)metric space), residual sets form a filter.

For technical reasons, we define residual in any topological space but the definition agrees with the description above only in Baire spaces.

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

source

def is_Gδ {α : Type u_1} [topological_space α] (s : set α) :

Prop

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

Equations

is_Gδ s = ∃ (T : set (set α)), (∀ (t : set α), t ∈ T → is_open t) ∧ T.countable ∧ s = ⋂₀T

source

theorem is_open.is_Gδ {α : Type u_1} [topological_space α] {s : set α} (h : is_open s) :

is_Gδ s

An open set is a Gδ set.

source

theorem is_Gδ_univ {α : Type u_1} [topological_space α] :

is_Gδ set.univ

source

theorem is_Gδ_bInter_of_open {α : Type u_1} {ι : Type u_4} [topological_space α] {I : set ι} (hI : I.countable) {f : ι → set α} (hf : ∀ (i : ι), i ∈ I → is_open (f i)) :

is_Gδ (⋂ (i : ι) (H : i ∈ I), f i)

source

theorem is_Gδ_Inter_of_open {α : Type u_1} {ι : Type u_4} [topological_space α] [encodable ι] {f : ι → set α} (hf : ∀ (i : ι), is_open (f i)) :

is_Gδ (⋂ (i : ι), f i)

source

theorem is_Gδ_sInter {α : Type u_1} [topological_space α] {S : set (set α)} (h : ∀ (s : set α), s ∈ S → is_Gδ s) (hS : S.countable) :

is_Gδ (⋂₀S)

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

source

theorem is_Gδ_Inter {α : Type u_1} {ι : Type u_4} [topological_space α] [encodable ι] {s : ι → set α} (hs : ∀ (i : ι), is_Gδ (s i)) :

is_Gδ (⋂ (i : ι), s i)

source

theorem is_Gδ_bInter {α : Type u_1} {ι : Type u_4} [topological_space α] {s : set ι} (hs : s.countable) {t : Π (i : ι), i ∈ s → set α} (ht : ∀ (i : ι) (H : i ∈ s), is_Gδ (t i H)) :

is_Gδ (⋂ (i : ι) (H : i ∈ s), t i H)

source

theorem is_Gδ.inter {α : Type u_1} [topological_space α] {s t : set α} (hs : is_Gδ s) (ht : is_Gδ t) :

is_Gδ (s ∩ t)

source

theorem is_Gδ.union {α : Type u_1} [topological_space α] {s t : set α} (hs : is_Gδ s) (ht : is_Gδ t) :

is_Gδ (s ∪ t)

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

source

theorem is_Gδ_set_of_continuous_at_of_countably_generated_uniformity {α : Type u_1} {β : Type u_2} [topological_space α] [uniform_space β] (hU : (𝓤 β).is_countably_generated) (f : α → β) :

is_Gδ {x : α | continuous_at f x}

source

theorem is_Gδ_set_of_continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [emetric_space β] (f : α → β) :

is_Gδ {x : α | continuous_at f x}

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

source

def residual (α : Type u_1) [topological_space α] :

filter α

A set s is called residual if it includes a dense Gδ set. If α is a Baire space (e.g., a complete metric space), then residual sets form a filter, see mem_residual.

For technical reasons we define the filter residual in any topological space but in a non-Baire space it is not useful because it may contain some non-residual sets.

Equations

residual α = ⨅ (t : set α) (ht : is_Gδ t) (ht' : dense t), 𝓟 t