Documentation

Mathlib.Topology.Compactness.SigmaCompact

Sigma-compactness in topological spaces #

Main definitions #

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

A subset s ⊆ X is called σ-compact if it is the union of countably many compact sets.

Equations
Instances For
    theorem IsCompact.isSigmaCompact {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) :

    Compact sets are σ-compact.

    @[simp]

    The empty set is σ-compact.

    theorem isSigmaCompact_iUnion_of_isCompact {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] [hι : Countable ι] (s : ιSet X) (hcomp : ∀ (i : ι), IsCompact (s i)) :
    IsSigmaCompact (⋃ (i : ι), s i)

    Countable unions of compact sets are σ-compact.

    theorem isSigmaCompact_sUnion_of_isCompact {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} (hc : S.Countable) (hcomp : sS, IsCompact s) :

    Countable unions of compact sets are σ-compact.

    theorem isSigmaCompact_iUnion {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] [Countable ι] (s : ιSet X) (hcomp : ∀ (i : ι), IsSigmaCompact (s i)) :
    IsSigmaCompact (⋃ (i : ι), s i)

    Countable unions of σ-compact sets are σ-compact.

    theorem isSigmaCompact_sUnion {X : Type u_1} [TopologicalSpace X] (S : Set (Set X)) (hc : S.Countable) (hcomp : ∀ (s : S), IsSigmaCompact s) :

    Countable unions of σ-compact sets are σ-compact.

    theorem isSigmaCompact_biUnion {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {s : Set ι} {S : ιSet X} (hc : s.Countable) (hcomp : is, IsSigmaCompact (S i)) :
    IsSigmaCompact (⋃ is, S i)

    Countable unions of σ-compact sets are σ-compact.

    theorem IsSigmaCompact.of_isClosed_subset {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} (ht : IsSigmaCompact t) (hs : IsClosed s) (h : s t) :

    A closed subset of a σ-compact set is σ-compact.

    theorem IsSigmaCompact.image_of_continuousOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} (hs : IsSigmaCompact s) (hf : ContinuousOn f s) :

    If s is σ-compact and f is continuous on s, f(s) is σ-compact.

    theorem IsSigmaCompact.image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : Continuous f) {s : Set X} (hs : IsSigmaCompact s) :

    If s is σ-compact and f continuous, f(s) is σ-compact.

    theorem Inducing.isSigmaCompact_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} (hf : Inducing f) :

    If f : X → Y is Inducing, the image f '' s of a set s is σ-compact if and only s is σ-compact.

    theorem Embedding.isSigmaCompact_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} (hf : Embedding f) :

    If f : X → Y is an Embedding, the image f '' s of a set s is σ-compact if and only s is σ-compact.

    theorem Subtype.isSigmaCompact_iff {X : Type u_1} [TopologicalSpace X] {p : XProp} {s : Set { a : X // p a }} :

    Sets of subtype are σ-compact iff the image under a coercion is.

    A σ-compact space is a space that is the union of a countable collection of compact subspaces. Note that a locally compact separable T₂ space need not be σ-compact. The sequence can be extracted using compactCovering.

    Instances
      theorem SigmaCompactSpace.isSigmaCompact_univ {X : Type u_4} :
      ∀ {inst : TopologicalSpace X} [self : SigmaCompactSpace X], IsSigmaCompact Set.univ

      In a σ-compact space, Set.univ is a σ-compact set.

      A topological space is σ-compact iff univ is σ-compact.

      In a σ-compact space, univ is σ-compact.

      theorem SigmaCompactSpace_iff_exists_compact_covering {X : Type u_1} [TopologicalSpace X] :
      SigmaCompactSpace X ∃ (K : Set X), (∀ (n : ), IsCompact (K n)) ⋃ (n : ), K n = Set.univ

      A topological space is σ-compact iff there exists a countable collection of compact subspaces that cover the entire space.

      theorem SigmaCompactSpace.exists_compact_covering {X : Type u_1} [TopologicalSpace X] [h : SigmaCompactSpace X] :
      ∃ (K : Set X), (∀ (n : ), IsCompact (K n)) ⋃ (n : ), K n = Set.univ
      theorem isSigmaCompact_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : Continuous f) [SigmaCompactSpace X] :

      If X is σ-compact, im f is σ-compact.

      A subset s is σ-compact iff s (with the subspace topology) is a σ-compact space.

      @[instance 200]
      Equations
      • =
      theorem SigmaCompactSpace.of_countable {X : Type u_1} [TopologicalSpace X] (S : Set (Set X)) (Hc : S.Countable) (Hcomp : sS, IsCompact s) (HU : ⋃₀ S = Set.univ) :

      A choice of compact covering for a σ-compact space, chosen to be monotone.

      Equations
      Instances For
        theorem iUnion_compactCovering (X : Type u_1) [TopologicalSpace X] [SigmaCompactSpace X] :
        ⋃ (n : ), compactCovering X n = Set.univ
        theorem compactCovering_subset (X : Type u_1) [TopologicalSpace X] [SigmaCompactSpace X] ⦃m : ⦃n : (h : m n) :
        instance instSigmaCompactSpaceForallOfFinite {ι : Type u_3} [Finite ι] {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), SigmaCompactSpace (X i)] :
        SigmaCompactSpace ((i : ι) → X i)
        Equations
        • =
        instance instSigmaCompactSpaceSigmaOfCountable {ι : Type u_3} [Countable ι] {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), SigmaCompactSpace (X i)] :
        SigmaCompactSpace ((i : ι) × X i)
        Equations
        • =
        theorem LocallyFinite.countable_univ {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] [SigmaCompactSpace X] {f : ιSet X} (hf : LocallyFinite f) (hne : ∀ (i : ι), (f i).Nonempty) :
        Set.univ.Countable

        If X is a σ-compact space, then a locally finite family of nonempty sets of X can have only countably many elements, Set.Countable version.

        noncomputable def LocallyFinite.encodable {X : Type u_1} [TopologicalSpace X] [SigmaCompactSpace X] {ι : Type u_4} {f : ιSet X} (hf : LocallyFinite f) (hne : ∀ (i : ι), (f i).Nonempty) :

        If f : ι → Set X is a locally finite covering of a σ-compact topological space by nonempty sets, then the index type ι is encodable.

        Equations
        Instances For
          theorem countable_cover_nhdsWithin_of_sigma_compact {X : Type u_1} [TopologicalSpace X] [SigmaCompactSpace X] {f : XSet X} {s : Set X} (hs : IsClosed s) (hf : xs, f x nhdsWithin x s) :
          ts, t.Countable s xt, f x

          In a topological space with sigma compact topology, if f is a function that sends each point x of a closed set s to a neighborhood of x within s, then for some countable set t ⊆ s, the neighborhoods f x, x ∈ t, cover the whole set s.

          theorem countable_cover_nhds_of_sigma_compact {X : Type u_1} [TopologicalSpace X] [SigmaCompactSpace X] {f : XSet X} (hf : ∀ (x : X), f x nhds x) :
          ∃ (s : Set X), s.Countable xs, f x = Set.univ

          In a topological space with sigma compact topology, if f is a function that sends each point x to a neighborhood of x, then for some countable set s, the neighborhoods f x, x ∈ s, cover the whole space.

          structure CompactExhaustion (X : Type u_4) [TopologicalSpace X] :
          Type u_4

          An exhaustion by compact sets of a topological space is a sequence of compact sets K n such that K n ⊆ interior (K (n + 1)) and ⋃ n, K n = univ.

          If X is a locally compact sigma compact space, then CompactExhaustion.choice X provides a choice of an exhaustion by compact sets. This choice is also available as (default : CompactExhaustion X).

          • toFun : Set X

            The sequence of compact sets that form a compact exhaustion.

          • isCompact' : ∀ (n : ), IsCompact (self.toFun n)

            The sets in the compact exhaustion are in fact compact.

          • subset_interior_succ' : ∀ (n : ), self.toFun n interior (self.toFun (n + 1))

            The sets in the compact exhaustion form a sequence: each set is contained in the interior of the next.

          • iUnion_eq' : ⋃ (n : ), self.toFun n = Set.univ

            The union of all sets in a compact exhaustion equals the entire space.

          Instances For
            theorem CompactExhaustion.isCompact' {X : Type u_4} [TopologicalSpace X] (self : CompactExhaustion X) (n : ) :
            IsCompact (self.toFun n)

            The sets in the compact exhaustion are in fact compact.

            theorem CompactExhaustion.subset_interior_succ' {X : Type u_4} [TopologicalSpace X] (self : CompactExhaustion X) (n : ) :
            self.toFun n interior (self.toFun (n + 1))

            The sets in the compact exhaustion form a sequence: each set is contained in the interior of the next.

            theorem CompactExhaustion.iUnion_eq' {X : Type u_4} [TopologicalSpace X] (self : CompactExhaustion X) :
            ⋃ (n : ), self.toFun n = Set.univ

            The union of all sets in a compact exhaustion equals the entire space.

            Equations
            • CompactExhaustion.instFunLikeNatSet = { coe := CompactExhaustion.toFun, coe_injective' := }
            @[simp]
            theorem CompactExhaustion.toFun_eq_coe {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) :
            K.toFun = K
            theorem CompactExhaustion.subset {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) ⦃m : ⦃n : (h : m n) :
            K m K n
            theorem CompactExhaustion.subset_succ {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (n : ) :
            K n K (n + 1)
            theorem CompactExhaustion.subset_interior {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) ⦃m : ⦃n : (h : m < n) :
            K m interior (K n)
            theorem CompactExhaustion.iUnion_eq {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) :
            ⋃ (n : ), K n = Set.univ
            theorem CompactExhaustion.exists_mem {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (x : X) :
            ∃ (n : ), x K n
            theorem CompactExhaustion.exists_superset_of_isCompact {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) {s : Set X} (hs : IsCompact s) :
            ∃ (n : ), s K n

            A compact exhaustion eventually covers any compact set.

            noncomputable def CompactExhaustion.find {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (x : X) :

            The minimal n such that x ∈ K n.

            Equations
            Instances For
              theorem CompactExhaustion.mem_find {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (x : X) :
              x K (K.find x)
              theorem CompactExhaustion.mem_iff_find_le {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) {x : X} {n : } :
              x K n K.find x n

              Prepend the empty set to a compact exhaustion K n.

              Equations
              • K.shiftr = { toFun := fun (n : ) => Nat.casesOn n K, isCompact' := , subset_interior_succ' := , iUnion_eq' := }
              Instances For
                @[simp]
                theorem CompactExhaustion.find_shiftr {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (x : X) :
                K.shiftr.find x = K.find x + 1
                theorem CompactExhaustion.mem_diff_shiftr_find {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (x : X) :
                x K.shiftr (K.find x + 1) \ K.shiftr (K.find x)

                A choice of an exhaustion by compact sets of a weakly locally compact σ-compact space.

                Equations
                Instances For
                  Equations