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.

• IsNowhereDense: a set is called nowhere dense iff its closure has empty interior

• IsMeagre: a set s is called meagre iff its complement is residual

Main results

We prove that finite or countable intersections of Gδ sets are Gδ sets. We also prove that the continuity set of a function from a topological space to an (e)metric space is a Gδ set.

• isClosed_isNowhereDense_iff_compl: a closed set is nowhere dense iff its complement is open and dense
• isMeagre_iff_countable_union_isNowhereDense: a set is meagre iff it is contained in a countable union of nowhere dense sets
• subsets of meagre sets are meagre; countable unions of meagre sets are meagre

Tags

Gδ set, residual set, nowhere dense set, meagre set

def IsGδ {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

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

Equations

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

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

An open set is a Gδ set.

@[simp]

theorem IsGδ.empty {X : Type u_1} [TopologicalSpace X] : IsGδ ∅

@[deprecated IsGδ.empty]

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

Alias of IsGδ.empty.

@[simp]

theorem IsGδ.univ {X : Type u_1} [TopologicalSpace X] : IsGδ Set.univ

@[deprecated IsGδ.univ]

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

Alias of IsGδ.univ.

theorem IsGδ.biInter_of_isOpen {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {I : Set ι} (hI : Set.Countable I) {f : ι → Set X} (hf : ∀ i ∈ I, IsOpen (f i)) : IsGδ (⋂ i ∈ I, f i)

@[deprecated IsGδ.biInter_of_isOpen]

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

Alias of IsGδ.biInter_of_isOpen.

theorem IsGδ.iInter_of_isOpen {X : Type u_1} {ι' : Sort u_4} [TopologicalSpace X] [Countable ι'] {f : ι' → Set X} (hf : ∀ (i : ι'), IsOpen (f i)) : IsGδ (⋂ (i : ι'), f i)

@[deprecated IsGδ.iInter_of_isOpen]

theorem isGδ_iInter_of_isOpen {X : Type u_1} {ι' : Sort u_4} [TopologicalSpace X] [Countable ι'] {f : ι' → Set X} (hf : ∀ (i : ι'), IsOpen (f i)) : IsGδ (⋂ (i : ι'), f i)

Alias of IsGδ.iInter_of_isOpen.

theorem isGδ_iff_eq_iInter_nat {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsGδ s ↔ ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen (f n)) ∧ s = ⋂ (n : ℕ), f n

theorem IsGδ.eq_iInter_nat {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsGδ s → ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen (f n)) ∧ s = ⋂ (n : ℕ), f n

Alias of the forward direction of isGδ_iff_eq_iInter_nat.

theorem IsGδ.iInter {X : Type u_1} {ι' : Sort u_4} [TopologicalSpace X] [Countable ι'] {s : ι' → Set X} (hs : ∀ (i : ι'), IsGδ (s i)) : IsGδ (⋂ (i : ι'), s i)

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

@[deprecated IsGδ.iInter]

theorem isGδ_iInter {X : Type u_1} {ι' : Sort u_4} [TopologicalSpace X] [Countable ι'] {s : ι' → Set X} (hs : ∀ (i : ι'), IsGδ (s i)) : IsGδ (⋂ (i : ι'), s i)

Alias of IsGδ.iInter.

---

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

theorem IsGδ.biInter {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {s : Set ι} (hs : Set.Countable s) {t : (i : ι) → i ∈ s → Set X} (ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)) : IsGδ (⋂ (i : ι), ⋂ (h : i ∈ s), t i h)

@[deprecated IsGδ.biInter]

theorem isGδ_biInter {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {s : Set ι} (hs : Set.Countable s) {t : (i : ι) → i ∈ s → Set X} (ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)) : IsGδ (⋂ (i : ι), ⋂ (h : i ∈ s), t i h)

Alias of IsGδ.biInter.

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

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

@[deprecated IsGδ.sInter]

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

Alias of IsGδ.sInter.

---

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

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

theorem IsGδ.union {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsGδ s) (ht : IsGδ t) : IsGδ (s ∪ t)

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

theorem IsGδ.sUnion {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} (hS : Set.Finite S) (h : ∀ s ∈ S, IsGδ s) : IsGδ (⋃₀ S)

The union of finitely many Gδ sets is a Gδ set, Set.sUnion version.

theorem IsGδ.biUnion {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {s : Set ι} (hs : Set.Finite s) {f : ι → Set X} (h : ∀ i ∈ s, IsGδ (f i)) : IsGδ (⋃ i ∈ s, f i)

The union of finitely many Gδ sets is a Gδ set, bounded indexed union version.

@[deprecated IsGδ.biUnion]

theorem isGδ_biUnion {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {s : Set ι} (hs : Set.Finite s) {f : ι → Set X} (h : ∀ i ∈ s, IsGδ (f i)) : IsGδ (⋃ i ∈ s, f i)

Alias of IsGδ.biUnion.

---

The union of finitely many Gδ sets is a Gδ set, bounded indexed union version.

theorem IsGδ.iUnion {X : Type u_1} {ι' : Sort u_4} [TopologicalSpace X] [Finite ι'] {f : ι' → Set X} (h : ∀ (i : ι'), IsGδ (f i)) : IsGδ (⋃ (i : ι'), f i)

The union of finitely many Gδ sets is a Gδ set, bounded indexed union version.

theorem IsClosed.isGδ {X : Type u_5} [UniformSpace X] [Filter.IsCountablyGenerated (uniformity X)] {s : Set X} (hs : IsClosed s) : IsGδ s

theorem IsGδ.compl_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] (x : X) : IsGδ {x}ᶜ

@[deprecated IsGδ.compl_singleton]

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

Alias of IsGδ.compl_singleton.

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

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

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

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

theorem IsGδ.singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] [FirstCountableTopology X] (x : X) : IsGδ {x}

@[deprecated IsGδ.singleton]

theorem isGδ_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] [FirstCountableTopology X] (x : X) : IsGδ {x}

Alias of IsGδ.singleton.

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

theorem IsGδ.setOf_continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [UniformSpace Y] [Filter.IsCountablyGenerated (uniformity Y)] (f : X → Y) : IsGδ {x : X | ContinuousAt f x}

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

@[deprecated IsGδ.setOf_continuousAt]

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

Alias of IsGδ.setOf_continuousAt.

---

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

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

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

Equations

• residual X = Filter.countableGenerate {t : Set X | IsOpen t ∧ Dense t}

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

Equations

• ⋯ = ⋯

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

Dense open sets are residual.

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

Dense Gδ sets are residual.

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

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

def IsNowhereDense {X : Type u_5} [TopologicalSpace X] (s : Set X) : Prop

A set is called nowhere dense iff its closure has empty interior.

Equations

• IsNowhereDense s = (interior (closure s) = ∅)

@[simp]

theorem isNowhereDense_empty {X : Type u_5} [TopologicalSpace X] : IsNowhereDense ∅

The empty set is nowhere dense.

theorem IsClosed.isNowhereDense_iff {X : Type u_5} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) : IsNowhereDense s ↔ interior s = ∅

A closed set is nowhere dense iff its interior is empty.

theorem IsNowhereDense.closure {X : Type u_5} [TopologicalSpace X] {s : Set X} (hs : IsNowhereDense s) : IsNowhereDense (closure s)

If a set s is nowhere dense, so is its closure.

theorem IsNowhereDense.subset_of_closed_isNowhereDense {X : Type u_5} [TopologicalSpace X] {s : Set X} (hs : IsNowhereDense s) : ∃ (t : Set X), s ⊆ t ∧ IsNowhereDense t ∧ IsClosed t

A nowhere dense set s is contained in a closed nowhere dense set (namely, its closure).

theorem isClosed_isNowhereDense_iff_compl {X : Type u_5} [TopologicalSpace X] {s : Set X} : IsClosed s ∧ IsNowhereDense s ↔ IsOpen sᶜ ∧ Dense sᶜ

A set s is closed and nowhere dense iff its complement sᶜ is open and dense.

def IsMeagre {X : Type u_5} [TopologicalSpace X] (s : Set X) : Prop

A set is called meagre iff its complement is a residual (or comeagre) set.

Equations

• IsMeagre s = (sᶜ ∈ residual X)

theorem meagre_empty {X : Type u_5} [TopologicalSpace X] : IsMeagre ∅

The empty set is meagre.

theorem IsMeagre.mono {X : Type u_5} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsMeagre s) (hts : t ⊆ s) : IsMeagre t

Subsets of meagre sets are meagre.

theorem IsMeagre.inter {X : Type u_5} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsMeagre s) : IsMeagre (s ∩ t)

An intersection with a meagre set is meagre.

theorem isMeagre_iUnion {X : Type u_5} [TopologicalSpace X] {s : ℕ → Set X} (hs : ∀ (n : ℕ), IsMeagre (s n)) : IsMeagre (⋃ (n : ℕ), s n)

A countable union of meagre sets is meagre.

theorem isMeagre_iff_countable_union_isNowhereDense {X : Type u_5} [TopologicalSpace X] {s : Set X} : IsMeagre s ↔ ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ Set.Countable S ∧ s ⊆ ⋃₀ S

A set is meagre iff it is contained in a countable union of nowhere dense sets.