mathlib documentation

topology.G_delta

Gδ sets #

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

Main definitions #

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
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