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

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

Equations
Instances For
theorem IsOpen.isGδ {X : Type u_1} [] {s : Set X} (h : ) :

An open set is a Gδ set.

@[simp]
theorem IsGδ.empty {X : Type u_1} [] :
@[deprecated IsGδ.empty]
theorem isGδ_empty {X : Type u_1} [] :

Alias of IsGδ.empty.

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

Alias of IsGδ.univ.

theorem IsGδ.biInter_of_isOpen {X : Type u_1} {ι : Type u_3} [] {I : Set ι} (hI : I.Countable) {f : ιSet X} (hf : iI, IsOpen (f i)) :
IsGδ (iI, f i)
@[deprecated IsGδ.biInter_of_isOpen]
theorem isGδ_biInter_of_isOpen {X : Type u_1} {ι : Type u_3} [] {I : Set ι} (hI : I.Countable) {f : ιSet X} (hf : iI, IsOpen (f i)) :
IsGδ (iI, f i)

Alias of IsGδ.biInter_of_isOpen.

theorem IsGδ.iInter_of_isOpen {X : Type u_1} {ι' : Sort u_4} [] [] {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} [] [] {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} [] {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} [] {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} [] [] {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} [] [] {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} [] {s : Set ι} (hs : s.Countable) {t : (i : ι) → i sSet 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} [] {s : Set ι} (hs : s.Countable) {t : (i : ι) → i sSet 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} [] {S : Set (Set X)} (h : sS, IsGδ s) (hS : S.Countable) :

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

@[deprecated IsGδ.sInter]
theorem isGδ_sInter {X : Type u_1} [] {S : Set (Set X)} (h : sS, IsGδ s) (hS : S.Countable) :

Alias of IsGδ.sInter.

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

theorem IsGδ.inter {X : Type u_1} [] {s : Set X} {t : Set X} (hs : IsGδ s) (ht : IsGδ t) :
IsGδ (s t)
theorem IsGδ.union {X : Type u_1} [] {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} [] {S : Set (Set X)} (hS : S.Finite) (h : sS, 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} [] {s : Set ι} (hs : s.Finite) {f : ιSet X} (h : is, IsGδ (f i)) :
IsGδ (is, 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} [] {s : Set ι} (hs : s.Finite) {f : ιSet X} (h : is, IsGδ (f i)) :
IsGδ (is, 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} [] [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} [] [().IsCountablyGenerated] {s : Set X} (hs : ) :
theorem IsGδ.setOf_continuousAt {X : Type u_1} {Y : Type u_2} [] [] [().IsCountablyGenerated] (f : XY) :
IsGδ {x : 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} [] [] [().IsCountablyGenerated] (f : XY) :
IsGδ {x : 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) [] :

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

Equations
Instances For
instance countableInterFilter_residual {X : Type u_1} [] :
Equations
• =
theorem residual_of_dense_open {X : Type u_1} [] {s : Set X} (ho : ) (hd : ) :
s

Dense open sets are residual.

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

Dense Gδ sets are residual.

theorem mem_residual_iff {X : Type u_1} [] {s : Set X} :
s ∃ (S : Set (Set X)), (tS, ) (tS, ) S.Countable ⋂₀ S s

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

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

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

Equations
Instances For
@[simp]
theorem isNowhereDense_empty {X : Type u_5} [] :

The empty set is nowhere dense.

theorem IsClosed.isNowhereDense_iff {X : Type u_5} [] {s : Set X} (hs : ) :

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

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

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

theorem IsNowhereDense.subset_of_closed_isNowhereDense {X : Type u_5} [] {s : Set X} (hs : ) :
∃ (t : Set X), s 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} [] {s : Set X} :

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

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

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

Equations
Instances For
theorem meagre_empty {X : Type u_5} [] :

The empty set is meagre.

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

Subsets of meagre sets are meagre.

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

An intersection with a meagre set is meagre.

theorem isMeagre_iUnion {X : Type u_5} [] {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} [] {s : Set X} :
∃ (S : Set (Set X)), (tS, ) S.Countable s ⋃₀ S

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