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.

• 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

See Mathlib.Topology.GDelta.UniformSpace for the proof that continuity set of a function from a topological space to a uniform space is a Gδ set.

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) ∧ T.Countable ∧ 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 : I.Countable) {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 : I.Countable) {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 : s.Countable) {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 : s.Countable) {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 : S.Countable) : 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 : S.Countable) : 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 : S.Finite) (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 : s.Finite) {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 : s.Finite) {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.

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) ∧ S.Countable ∧ ⋂₀ 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) ∧ S.Countable ∧ s ⊆ ⋃₀ S

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