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} [TopologicalSpace α] (s : Set α) : Prop

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

Equations

• IsGδ s = ∃ T, (∀ (t : Set α), t ∈ T → IsOpen t) ∧ Set.Countable T ∧ s = ⋂₀ T

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

An open set is a Gδ set.

@[simp]

theorem isGδ_empty {α : Type u_1} [TopologicalSpace α] : IsGδ ∅

@[simp]

theorem isGδ_univ {α : Type u_1} [TopologicalSpace α] : IsGδ Set.univ

theorem isGδ_biInter_of_open {α : Type u_1} {ι : Type u_4} [TopologicalSpace α] {I : Set ι} (hI : Set.Countable I) {f : ι → Set α} (hf : ∀ (i : ι), i ∈ I → IsOpen (f i)) : IsGδ (⋂ (i : ι) (_ : i ∈ I), f i)

theorem isGδ_iInter_of_open {α : Type u_1} {ι : Type u_4} [TopologicalSpace α] [Encodable ι] {f : ι → Set α} (hf : ∀ (i : ι), IsOpen (f i)) : IsGδ (⋂ (i : ι), f i)

theorem isGδ_iInter {α : Type u_1} {ι : Type u_4} [TopologicalSpace α] [Encodable ι] {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} [TopologicalSpace α] {s : Set ι} (hs : Set.Countable s) {t : (i : ι) → i ∈ s → Set α} (ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)) : IsGδ (⋂ (i : ι) (h : i ∈ s), t i h)

theorem isGδ_sInter {α : Type u_1} [TopologicalSpace α] {S : Set (Set α)} (h : ∀ (s : Set α), s ∈ S → IsGδ s) (hS : Set.Countable S) : IsGδ (⋂₀ S)

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

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

theorem IsGδ.union {α : Type u_1} [TopologicalSpace α] {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} [TopologicalSpace α] {s : Set ι} (hs : Set.Finite s) {f : ι → Set α} (h : ∀ (i : ι), i ∈ s → IsGδ (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} [UniformSpace α] [Filter.IsCountablyGenerated (uniformity α)] {s : Set α} (hs : IsClosed s) : IsGδ s

theorem isGδ_compl_singleton {α : Type u_1} [TopologicalSpace α] [T1Space α] (a : α) : IsGδ {a}ᶜ

theorem Set.Countable.isGδ_compl {α : Type u_1} [TopologicalSpace α] [T1Space α] {s : Set α} (hs : Set.Countable s) : IsGδ sᶜ

theorem Set.Finite.isGδ_compl {α : Type u_1} [TopologicalSpace α] [T1Space α] {s : Set α} (hs : Set.Finite s) : IsGδ sᶜ

theorem Set.Subsingleton.isGδ_compl {α : Type u_1} [TopologicalSpace α] [T1Space α] {s : Set α} (hs : Set.Subsingleton s) : IsGδ sᶜ

theorem Finset.isGδ_compl {α : Type u_1} [TopologicalSpace α] [T1Space α] (s : Finset α) : IsGδ (↑s)ᶜ

theorem isGδ_singleton {α : Type u_1} [TopologicalSpace α] [T1Space α] [TopologicalSpace.FirstCountableTopology α] (a : α) : IsGδ {a}

theorem Set.Finite.isGδ {α : Type u_1} [TopologicalSpace α] [T1Space α] [TopologicalSpace.FirstCountableTopology α] {s : Set α} (hs : Set.Finite s) : IsGδ s

theorem isGδ_setOf_continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] [Filter.IsCountablyGenerated (uniformity β)] (f : α → β) : IsGδ {x | ContinuousAt f x}

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

def residual (α : Type u_5) [TopologicalSpace α] : Filter α

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

Equations

• residual α = Filter.countableGenerate {t | IsOpen t ∧ Dense t}

instance countableInterFilter_residual {α : Type u_1} [TopologicalSpace α] : CountableInterFilter (residual α)

Equations

• @countableInterFilter_residual = @countableInterFilter_residual.proof_1

theorem residual_of_dense_open {α : Type u_1} [TopologicalSpace α] {s : Set α} (ho : IsOpen s) (hd : Dense s) : s ∈ residual α

Dense open sets are residual.

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

Dense Gδ sets are residual.

theorem mem_residual_iff {α : Type u_1} [TopologicalSpace α] {s : Set α} : s ∈ residual α ↔ ∃ S, (∀ (t : Set α), t ∈ S → IsOpen t) ∧ (∀ (t : Set α), t ∈ S → Dense t) ∧ Set.Countable S ∧ ⋂₀ S ⊆ s

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