Documentation

Mathlib.Topology.CWComplex.Classical.Basic

CW complexes #

This file defines (relative) CW complexes and proves basic properties about them using the classical approach of Whitehead.

A CW complex is a topological space that is made by gluing closed disks of different dimensions together.

Main definitions #

Main statements #

Implementation notes #

References #

class Topology.RelCWComplex {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) :
Type (u + 1)

A CW complex of a topological space X relative to another subspace D is the data of its n-cells cell n i for each n : ℕ along with attaching maps that satisfy a number of properties with the most important being closure-finiteness (mapsTo) and weak topology (closed'). Note that this definition requires C and D to be closed subspaces. If C is not closed choose X to be C.

Instances
    @[deprecated Topology.RelCWComplex.mapsTo (since := "2025-02-20")]
    theorem Topology.RelCWComplex.mapsto {X : Type u} {inst✝ : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : RelCWComplex C D] (n : ) (i : cell C n) :
    ∃ (I : (m : ) → Finset (cell C m)), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (D ⋃ (m : ), ⋃ (_ : m < n), jI m, (map m j) '' Metric.closedBall 0 1)

    Alias of Topology.RelCWComplex.mapsTo.


    The boundary of a cell is contained in the union of the base with a finite union of closed cells of a lower dimension. Use RelCWComplex.cellFrontier_subset_base_union_finite_closedCell instead.

    class Topology.CWComplex {X : Type u} [TopologicalSpace X] (C : Set X) :
    Type (u + 1)

    Characterizing when a subspace C of a topological space X is a CW complex. Note that this requires C to be closed. If C is not closed choose X to be C.

    Instances
      @[instance 10000]
      Equations
      • One or more equations did not get rendered due to their size.

      A relative CW complex with an empty base is an absolute CW complex.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Topology.RelCWComplex.openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ) (i : cell C n) :
        Set X

        The open n-cell given by the index i. Use this instead of map n i '' ball 0 1 whenever possible.

        Equations
        Instances For
          def Topology.RelCWComplex.closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ) (i : cell C n) :
          Set X

          The closed n-cell given by the index i. Use this instead of map n i '' closedBall 0 1 whenever possible.

          Equations
          Instances For
            def Topology.RelCWComplex.cellFrontier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ) (i : cell C n) :
            Set X

            The boundary of the n-cell given by the index i. Use this instead of map n i '' sphere 0 1 whenever possible.

            Equations
            Instances For
              theorem Topology.CWComplex.mapsTo {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] (n : ) (i : cell C n) :
              ∃ (I : (m : ) → Finset (cell C m)), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ (m : ), ⋃ (_ : m < n), jI m, (map m j) '' Metric.closedBall 0 1)
              @[deprecated Topology.CWComplex.mapsTo (since := "2025-02-20")]
              theorem Topology.CWComplex.mapsto {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] (n : ) (i : cell C n) :
              ∃ (I : (m : ) → Finset (cell C m)), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ (m : ), ⋃ (_ : m < n), jI m, (map m j) '' Metric.closedBall 0 1)

              Alias of Topology.CWComplex.mapsTo.

              theorem Topology.RelCWComplex.pairwiseDisjoint {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] :
              Set.univ.PairwiseDisjoint fun (ni : (n : ) × cell C n) => openCell ni.fst ni.snd
              theorem Topology.RelCWComplex.disjointBase {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ) (i : cell C n) :
              theorem Topology.RelCWComplex.disjoint_openCell_of_ne {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n m : } {i : cell C n} {j : cell C m} (ne : n, i m, j) :
              theorem Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ) (i : cell C n) :
              ∃ (I : (m : ) → Finset (cell C m)), cellFrontier n i D ⋃ (m : ), ⋃ (_ : m < n), jI m, closedCell m j
              theorem Topology.CWComplex.cellFrontier_subset_finite_closedCell {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] (n : ) (i : cell C n) :
              ∃ (I : (m : ) → Finset (cell C m)), cellFrontier n i ⋃ (m : ), ⋃ (_ : m < n), jI m, closedCell m j
              theorem Topology.RelCWComplex.union {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] :
              D ⋃ (n : ), ⋃ (j : cell C n), closedCell n j = C
              theorem Topology.CWComplex.union {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] :
              ⋃ (n : ), ⋃ (j : cell C n), closedCell n j = C
              theorem Topology.RelCWComplex.map_zero_mem_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ) (i : cell C n) :
              (map n i) 0 openCell n i
              theorem Topology.RelCWComplex.map_zero_mem_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ) (i : cell C n) :
              (map n i) 0 closedCell n i
              theorem Topology.RelCWComplex.eq_of_eq_union_iUnion {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (I J : (n : ) → Set (cell C n)) (hIJ : D ⋃ (n : ), ⋃ (j : (I n)), openCell n j = D ⋃ (n : ), ⋃ (j : (J n)), openCell n j) :
              I = J
              theorem Topology.CWComplex.eq_of_eq_union_iUnion {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] (I J : (n : ) → Set (cell C n)) (hIJ : ⋃ (n : ), ⋃ (j : (I n)), openCell n j = ⋃ (n : ), ⋃ (j : (J n)), openCell n j) :
              I = J
              theorem Topology.RelCWComplex.isCompact_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n : } {i : cell C n} :
              theorem Topology.RelCWComplex.isClosed_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {n : } {i : cell C n} :
              theorem Topology.RelCWComplex.closed {X : Type u_1} [t : TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] [T2Space X] (A : Set X) (asubc : A C) :
              IsClosed A (∀ (n : ) (j : cell C n), IsClosed (A closedCell n j)) IsClosed (A D)
              theorem Topology.CWComplex.closed {X : Type u_1} [t : TopologicalSpace X] (C : Set X) [CWComplex C] [T2Space X] (A : Set X) (asubc : A C) :
              IsClosed A ∀ (n : ) (j : cell C n), IsClosed (A closedCell n j)
              theorem Topology.RelCWComplex.closedCell_subset_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ) (j : cell C n) :
              theorem Topology.RelCWComplex.openCell_subset_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ) (j : cell C n) :
              theorem Topology.RelCWComplex.openCell_zero_eq_singleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {j : cell C 0} :
              openCell 0 j = {(map 0 j) ![]}
              theorem Topology.RelCWComplex.union_iUnion_openCell_eq_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] :
              D ⋃ (n : ), ⋃ (j : cell C n), openCell n j = C
              theorem Topology.CWComplex.iUnion_openCell_eq_complex {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] :
              ⋃ (n : ), ⋃ (j : cell C n), openCell n j = C
              theorem Topology.RelCWComplex.eq_of_not_disjoint_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n : } {j : cell C n} {m : } {i : cell C m} (h : ¬Disjoint (openCell n j) (openCell m i)) :
              n, j = m, i

              The contrapositive of disjoint_openCell_of_ne.

              theorem Topology.RelCWComplex.disjoint_base_iUnion_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] :
              Disjoint D (⋃ (n : ), ⋃ (j : cell C n), openCell n j)
              theorem Topology.RelCWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {A : Set X} {n : } (hn : mn, ∀ (j : cell C m), IsClosed (A closedCell m j)) (j : cell C (n + 1)) (hD : IsClosed (A D)) :

              If for all m ≤ n and every i : cell C m the intersection A ∩ closedCell m j is closed and A ∩ D is closed then A ∩ cellFrontier (n + 1) j is closed for every j : cell C (n + 1).

              theorem Topology.CWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] [T2Space X] {A : Set X} {n : } (hn : mn, ∀ (j : cell C m), IsClosed (A closedCell m j)) (j : cell C (n + 1)) :
              theorem Topology.RelCWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {A : Set X} (hAC : A C) (hDA : IsClosed (A D)) (h : ∀ (n : ), 0 < n∀ (j : cell C n), IsClosed (A openCell n j) IsClosed (A closedCell n j)) :

              If for every cell either A ∩ openCell n j or A ∩ closedCell n j is closed then A is closed.

              theorem Topology.CWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] [T2Space X] {A : Set X} (hAC : A C) (h : ∀ (n : ), 0 < n∀ (j : cell C n), IsClosed (A openCell n j) IsClosed (A closedCell n j)) :

              If for every cell either A ∩ openCell n j or A ∩ closedCell n j is closed then A is closed.

              theorem Topology.RelCWComplex.cellFrontier_subset_finite_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ) (i : cell C n) :
              ∃ (I : (m : ) → Finset (cell C m)), cellFrontier n i D ⋃ (m : ), ⋃ (_ : m < n), jI m, openCell m j

              A version of cellFrontier_subset_base_union_finite_closedCell using open cells: The boundary of a cell is contained in a finite union of open cells of a lower dimension.

              theorem Topology.CWComplex.cellFrontier_subset_finite_openCell {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] (n : ) (i : cell C n) :
              ∃ (I : (m : ) → Finset (cell C m)), cellFrontier n i ⋃ (m : ), ⋃ (_ : m < n), jI m, openCell m j

              A version of cellFrontier_subset_finite_closedCell using open cells: The boundary of a cell is contained in a finite union of open cells of a lower dimension.

              structure Topology.RelCWComplex.Subcomplex {X : Type u_1} [t : TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] :
              Type u_1

              A subcomplex is a closed subspace of a CW complex that is the union of open cells of the CW complex.

              • carrier : Set X

                The underlying set of the subcomplex.

              • I (n : ) : Set (cell C n)

                The indexing set of cells of the subcomplex.

              • closed' : IsClosed self.carrier

                A subcomplex is closed.

              • union' : D ⋃ (n : ), ⋃ (j : (self.I n)), openCell n j = self.carrier

                The union of all open cells of the subcomplex equals the subcomplex.

              Instances For
                theorem Topology.RelCWComplex.Subcomplex.mem_carrier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {E : Subcomplex C} {x : X} :
                x E.carrier x E
                theorem Topology.RelCWComplex.Subcomplex.ext {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {E F : Subcomplex C} (h : ∀ (x : X), x E x F) :
                E = F
                theorem Topology.RelCWComplex.Subcomplex.ext_iff {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {E F : Subcomplex C} :
                E = F ∀ (x : X), x E x F
                theorem Topology.RelCWComplex.Subcomplex.eq_iff {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E F : Subcomplex C) :
                E = F E = F
                def Topology.RelCWComplex.Subcomplex.copy {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ) → Set (cell C n)) (hJ : J = E.I) :

                Copy of a Subcomplex with a new carrier equal to the old one. Useful to fix definitional equalities.

                Equations
                • E.copy F hF J hJ = { carrier := F, I := J, closed' := , union' := }
                Instances For
                  @[simp]
                  theorem Topology.RelCWComplex.Subcomplex.coe_copy {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ) → Set (cell C n)) (hJ : J = E.I) :
                  (E.copy F hF J hJ) = F
                  theorem Topology.RelCWComplex.Subcomplex.copy_eq {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ) → Set (cell C n)) (hJ : J = E.I) :
                  E.copy F hF J hJ = E
                  theorem Topology.RelCWComplex.Subcomplex.union {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) :
                  D ⋃ (n : ), ⋃ (j : (E.I n)), openCell n j = E
                  theorem Topology.CWComplex.Subcomplex.union {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] {E : Subcomplex C} :
                  ⋃ (n : ), ⋃ (j : (E.I n)), openCell n j = E
                  def Topology.RelCWComplex.Subcomplex.mk' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : (n : ) → Set (cell C n)) (closedCell_subset : ∀ (n : ) (i : (I n)), closedCell n i E) (union : D ⋃ (n : ), ⋃ (j : (I n)), openCell n j = E) :

                  An alternative version of Subcomplex.mk: Instead of requiring that E is closed it requires that for every cell of the subcomplex the corresponding closed cell is a subset of E.

                  Equations
                  Instances For
                    theorem Topology.RelCWComplex.Subcomplex.coe_mk' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : (n : ) → Set (cell C n)) (closedCell_subset : ∀ (n : ) (i : (I n)), closedCell n i E) (union : D ⋃ (n : ), ⋃ (j : (I n)), openCell n j = E) :
                    (mk' C E I closedCell_subset union) = E
                    theorem Topology.RelCWComplex.Subcomplex.mk'_I {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : (n : ) → Set (cell C n)) (closedCell_subset : ∀ (n : ) (i : (I n)), closedCell n i E) (union : D ⋃ (n : ), ⋃ (j : (I n)), openCell n j = E) (n : ) :
                    (mk' C E I closedCell_subset union).I n = I n
                    def Topology.CWComplex.Subcomplex.mk' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [CWComplex C] (E : Set X) (I : (n : ) → Set (cell C n)) (closedCell_subset : ∀ (n : ) (i : (I n)), closedCell n i E) (union : ⋃ (n : ), ⋃ (j : (I n)), openCell n j = E) :

                    An alternative version of Subcomplex.mk: Instead of requiring that E is closed it requires that for every cell of the subcomplex the corresponding closed cell is a subset of E.

                    Equations
                    Instances For
                      theorem Topology.CWComplex.Subcomplex.mk'_I {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [CWComplex C] (E : Set X) (I : (n : ) → Set (cell C n)) (closedCell_subset : ∀ (n : ) (i : (I n)), closedCell n i E) (union : ⋃ (n : ), ⋃ (j : (I n)), openCell n j = E) (n : ) :
                      (mk' C E I closedCell_subset union).I n = I n
                      theorem Topology.CWComplex.Subcomplex.coe_mk' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [CWComplex C] (E : Set X) (I : (n : ) → Set (cell C n)) (closedCell_subset : ∀ (n : ) (i : (I n)), closedCell n i E) (union : ⋃ (n : ), ⋃ (j : (I n)), openCell n j = E) :
                      (mk' C E I closedCell_subset union) = E
                      def Topology.RelCWComplex.Subcomplex.mk'' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : (n : ) → Set (cell C n)) [RelCWComplex E D] (union : D ⋃ (n : ), ⋃ (j : (I n)), openCell n j = E) :

                      An alternative version of Subcomplex.mk: Instead of requiring that E is closed it requires that E is a CW-complex.

                      Equations
                      Instances For
                        theorem Topology.RelCWComplex.Subcomplex.mk''_I {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : (n : ) → Set (cell C n)) [RelCWComplex E D] (union : D ⋃ (n : ), ⋃ (j : (I n)), openCell n j = E) (n : ) :
                        (mk'' C E I union).I n = I n
                        theorem Topology.RelCWComplex.Subcomplex.coe_mk'' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : (n : ) → Set (cell C n)) [RelCWComplex E D] (union : D ⋃ (n : ), ⋃ (j : (I n)), openCell n j = E) :
                        (mk'' C E I union) = E
                        def Topology.CWComplex.Subcomplex.mk'' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [h : CWComplex C] (E : Set X) (I : (n : ) → Set (cell C n)) [CWComplex E] (union : ⋃ (n : ), ⋃ (j : (I n)), openCell n j = E) :

                        An alternative version of Subcomplex.mk: Instead of requiring that E is closed it requires that E is a CW-complex.

                        Equations
                        Instances For
                          theorem Topology.CWComplex.Subcomplex.mk''_I {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [h : CWComplex C] (E : Set X) (I : (n : ) → Set (cell C n)) [CWComplex E] (union : ⋃ (n : ), ⋃ (j : (I n)), openCell n j = E) (n : ) :
                          (mk'' C E I union).I n = I n
                          theorem Topology.CWComplex.Subcomplex.coe_mk'' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [h : CWComplex C] (E : Set X) (I : (n : ) → Set (cell C n)) [CWComplex E] (union : ⋃ (n : ), ⋃ (j : (I n)), openCell n j = E) :
                          (mk'' C E I union) = E
                          @[irreducible]
                          def Topology.RelCWComplex.skeletonLT {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) :

                          A non-standard definition of the n-skeleton of a CW complex for n ∈ ℕ ∪ {∞}. This allows the base case of induction to be about the base instead of being about the union of the base and some points. The standard skeleton is defined in terms of skeletonLT. skeletonLT is preferred in statements. You should then derive the statement about skeleton.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem Topology.RelCWComplex.skeletonLT_I {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) (l : ) :
                            (skeletonLT C n).I l = {x : cell C l | l < n}
                            theorem Topology.RelCWComplex.coe_skeletonLT {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) :
                            (skeletonLT C n) = D ⋃ (m : ), ⋃ (_ : m < n), ⋃ (j : cell C m), closedCell m j
                            @[reducible, inline]
                            abbrev Topology.RelCWComplex.skeleton {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) :

                            The n-skeleton of a CW complex, for n ∈ ℕ ∪ {∞}. For statements use skeletonLT instead and then derive the statement about skeleton.

                            Equations
                            Instances For
                              @[simp]
                              theorem Topology.RelCWComplex.skeletonLT_top {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] :
                              (skeletonLT C ) = C
                              @[simp]
                              theorem Topology.RelCWComplex.skeleton_top {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] :
                              (skeleton C ) = C
                              theorem Topology.RelCWComplex.skeletonLT_mono {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n m : ℕ∞} (h : m n) :
                              (skeletonLT C m) (skeletonLT C n)
                              theorem Topology.RelCWComplex.skeleton_mono {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n m : ℕ∞} (h : m n) :
                              (skeleton C m) (skeleton C n)
                              theorem Topology.RelCWComplex.closedCell_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ) (j : cell C n) :
                              closedCell n j (skeletonLT C (n + 1))
                              theorem Topology.RelCWComplex.closedCell_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ) (j : cell C n) :
                              closedCell n j (skeleton C n)
                              theorem Topology.RelCWComplex.openCell_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ) (j : cell C n) :
                              openCell n j (skeletonLT C (n + 1))
                              theorem Topology.RelCWComplex.openCell_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ) (j : cell C n) :
                              openCell n j (skeleton C n)
                              theorem Topology.RelCWComplex.cellFrontier_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ) (j : cell C n) :
                              cellFrontier n j (skeletonLT C n)
                              theorem Topology.RelCWComplex.cellFrontier_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ) (j : cell C (n + 1)) :
                              cellFrontier (n + 1) j (skeleton C n)
                              theorem Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (l : ) :
                              ⋃ (j : cell C l), cellFrontier l j (skeletonLT C l)
                              theorem Topology.RelCWComplex.iUnion_cellFrontier_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (l : ) :
                              ⋃ (j : cell C l), cellFrontier l j (skeleton C l)
                              theorem Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ) :
                              (skeletonLT C n) ⋃ (j : cell C n), closedCell n j = (skeletonLT C (n + 1))
                              theorem Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ) :
                              (skeleton C n) ⋃ (j : cell C (n + 1)), closedCell (n + 1) j = (skeleton C (n + 1))
                              theorem Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ℕ∞) :
                              D ⋃ (m : ), ⋃ (_ : m < n), ⋃ (j : cell C m), openCell m j = (skeletonLT C n)

                              A version of the definition of skeletonLT with open cells.

                              theorem Topology.CWComplex.iUnion_openCell_eq_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] (n : ℕ∞) :
                              ⋃ (m : ), ⋃ (_ : m < n), ⋃ (j : cell C m), openCell m j = (skeletonLT C n)
                              theorem Topology.RelCWComplex.iUnion_openCell_eq_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ℕ∞) :
                              D ⋃ (m : ), ⋃ (_ : m < n + 1), ⋃ (j : cell C m), openCell m j = (skeleton C n)
                              theorem Topology.CWComplex.iUnion_openCell_eq_skeleton {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] (n : ℕ∞) :
                              ⋃ (m : ), ⋃ (_ : m < n + 1), ⋃ (j : cell C m), openCell m j = (skeleton C n)
                              theorem Topology.RelCWComplex.iUnion_skeletonLT_eq_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] :
                              ⋃ (n : ), (skeletonLT C n) = C
                              theorem Topology.RelCWComplex.iUnion_skeleton_eq_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] :
                              ⋃ (n : ), (skeleton C n) = C
                              theorem Topology.RelCWComplex.mem_skeletonLT_iff {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n : ℕ∞} {x : X} :
                              x skeletonLT C n x D ∃ (m : ) (_ : m < n) (j : cell C m), x openCell m j
                              theorem Topology.CWComplex.mem_skeletonLT_iff {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] {n : ℕ∞} {x : X} :
                              x skeletonLT C n ∃ (m : ) (_ : m < n) (j : cell C m), x openCell m j
                              theorem Topology.RelCWComplex.mem_skeleton_iff {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n : ℕ∞} {x : X} :
                              x skeleton C n x D ∃ (m : ) (_ : m n) (j : cell C m), x openCell m j
                              theorem Topology.CWComplex.exists_mem_openCell_of_mem_skeleton {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] {n : ℕ∞} {x : X} :
                              x skeleton C n ∃ (m : ) (_ : m n) (j : cell C m), x openCell m j
                              theorem Topology.RelCWComplex.disjoint_skeletonLT_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n : ℕ∞} {m : } {j : cell C m} (hnm : n m) :
                              Disjoint (↑(skeletonLT C n)) (openCell m j)

                              A skeleton and an open cell of a higher dimension are disjoint.

                              theorem Topology.RelCWComplex.disjoint_skeleton_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n : ℕ∞} {m : } {j : cell C m} (nlem : n < m) :
                              Disjoint (↑(skeleton C n)) (openCell m j)

                              A skeleton and an open cell of a higher dimension are disjoint.

                              theorem Topology.RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n : ℕ∞} {m : } {j : cell C m} (hnm : n m) :

                              A skeleton intersected with a closed cell of a higher dimension is the skeleton intersected with the boundary of the cell.