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

source
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

Instances For

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

An open set is a Gδ set.

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

source
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.

source
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)
source
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.

source
theorem IsGδ.inter {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hs : IsGδ s) (ht : IsGδ t) :
IsGδ (s ∩ t)
source
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.

source
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.

source
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.

source
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.

source
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}

Instances For

source
instance countableInterFilter_residual {X : Type u_1} [TopologicalSpace X] :
CountableInterFilter (residual X)
source
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.

source
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.

source
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.

source
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) = ∅)

Instances For

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

The empty set is nowhere dense.

source
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.

source
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.

source
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).

source
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.

source
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)

Instances For

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

The empty set is meagre.

source
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.

source
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.

source
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.

source
theorem isMeagre_iUnion {ι' : Sort u_4} {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.

source
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.

source
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.