Documentation

Mathlib.Topology.GDelta

sets #

In this file we define sets and prove their basic properties.

Main definitions #

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.

Tags #

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

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

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

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

    An open set is a Gδ set.

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

    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 : 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} [TopologicalSpace X] {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} [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 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} [TopologicalSpace X] {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} [TopologicalSpace X] {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} [TopologicalSpace X] {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} [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 : 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} [TopologicalSpace X] {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} [TopologicalSpace X] {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} [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] [(uniformity X).IsCountablyGenerated] {s : Set X} (hs : IsClosed s) :
    theorem IsGδ.setOf_continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [UniformSpace Y] [(uniformity Y).IsCountablyGenerated] (f : XY) :
    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] [(uniformity Y).IsCountablyGenerated] (f : XY) :
    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] :

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

    Equations
    Instances For
      theorem residual_of_dense_open {X : Type u_1} [TopologicalSpace X] {s : Set X} (ho : IsOpen s) (hd : Dense s) :

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

      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)), (tS, IsOpen t) (tS, 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) :

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

      Equations
      Instances For
        @[simp]

        The empty set is nowhere dense.

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

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

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

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

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

        Equations
        Instances For

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

          Subsets of meagre sets are meagre.

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

          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)), (tS, IsNowhereDense t) S.Countable s ⋃₀ S

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