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

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

@[simp]

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

is_Gδ ∅

source

@[simp]

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δ_Inter {α : Type u_1} {ι : Type u_4} [topological_space α] [encodable ι] {s : ι → set α} (hs : ∀ (i : ι), is_Gδ (s i)) :

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

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

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δ_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} [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δ_bUnion {α : Type u_1} {ι : Type u_4} [topological_space α] {s : set ι} (hs : s.finite) {f : ι → set α} (h : ∀ (i : ι), i ∈ s → is_Gδ (f i)) :

is_Gδ (⋃ (i : ι) (H : i ∈ s), f i)

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

source

theorem is_closed.is_Gδ {α : Type u_1} [uniform_space α] [(uniformity α).is_countably_generated] {s : set α} (hs : is_closed s) :

is_Gδ s

source

theorem is_Gδ_compl_singleton {α : Type u_1} [topological_space α] [t1_space α] (a : α) :

is_Gδ {a}ᶜ

source

theorem set.countable.is_Gδ_compl {α : Type u_1} [topological_space α] [t1_space α] {s : set α} (hs : s.countable) :

is_Gδ sᶜ

source

theorem set.finite.is_Gδ_compl {α : Type u_1} [topological_space α] [t1_space α] {s : set α} (hs : s.finite) :

is_Gδ sᶜ

source

theorem set.subsingleton.is_Gδ_compl {α : Type u_1} [topological_space α] [t1_space α] {s : set α} (hs : s.subsingleton) :

is_Gδ sᶜ

source

theorem finset.is_Gδ_compl {α : Type u_1} [topological_space α] [t1_space α] (s : finset α) :

is_Gδ (↑s)ᶜ

source

theorem is_Gδ_singleton {α : Type u_1} [topological_space α] [t1_space α] [topological_space.first_countable_topology α] (a : α) :

is_Gδ {a}

source

theorem set.finite.is_Gδ {α : Type u_1} [topological_space α] [t1_space α] [topological_space.first_countable_topology α] {s : set α} (hs : s.finite) :

is_Gδ s

source

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

is_Gδ {x : α | continuous_at f x}

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

source

@[protected, instance]

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

countable_Inter_filter (residual α)

source

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

filter α

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

Equations

residual α = filter.countable_generate {t : set α | is_open t ∧ dense t}

Instances for residual

source

@[protected, instance]

def countable_Inter_filter_residual {α : Type u_1} [topological_space α] :

countable_Inter_filter (residual α)

source

theorem residual_of_dense_open {α : Type u_1} [topological_space α] {s : set α} (ho : is_open s) (hd : dense s) :

s ∈ residual α

Dense open sets are residual.

source

theorem residual_of_dense_Gδ {α : Type u_1} [topological_space α] {s : set α} (ho : is_Gδ s) (hd : dense s) :

s ∈ residual α

Dense Gδ sets are residual.

source

theorem mem_residual_iff {α : Type u_1} [topological_space α] {s : set α} :

s ∈ residual α ↔ ∃ (S : set (set α)), (∀ (t : set α), t ∈ S → is_open t) ∧ (∀ (t : set α), t ∈ S → dense t) ∧ S.countable ∧ ⋂₀ S ⊆ s

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

Gδ sets #

Main definitions #

Main results #

Tags #

`Gδ` sets #