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/MetrizableSpace.lean for the proof that continuity set of a function from a topological space to a metrizable 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.

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

@[simp]

theorem IsGδ.univ {X : Type u_1} [TopologicalSpace X] : IsGδ Set.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)

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)

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.

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)

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.

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

theorem IsGδ.union {X : Type u_1} [TopologicalSpace X] {s 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.

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.

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

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.

@[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.

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

The empty set is meagre.

theorem IsMeagre.mono {X : Type u_5} [TopologicalSpace X] {s 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 t : Set X} (hs : IsMeagre s) : IsMeagre (s ∩ t)

An intersection with a meagre set is meagre.

theorem IsMeagre.union {X : Type u_5} [TopologicalSpace X] {s t : Set X} (hs : IsMeagre s) (ht : IsMeagre t) : IsMeagre (s ∪ t)

A union of two meagre sets is meagre.

theorem isMeagre_iUnion {ι : Type u_3} {X : Type u_5} [TopologicalSpace X] [Countable ι] {f : ι → Set X} (hs : ∀ (i : ι), IsMeagre (f i)) : IsMeagre (⋃ (i : ι), f i)

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.

theorem nonempty_of_not_isMeagre {X : Type u_5} [TopologicalSpace X] {s : Set X} (hs : ¬IsMeagre s) : s.Nonempty

A set of second category (i.e. non-meagre) is nonempty.