Documentation

Mathlib.Topology.CWComplex.Classical.Finite

Finiteness notions on CW complexes #

In this file we define what it means for a CW complex to be finite dimensional, of finite type or finite. We define constructors with relaxed conditions for CW complexes of finite type and finite CW complexes.

Main definitions #

Main statements #

source
๐Ÿ”ถ coverage
class Topology.RelCWComplex.FiniteDimensional {X : Type u} [TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] :
Prop

A CW complex is finite dimensional if cell C n is empty for all but finitely many n.

Instances
    source
    ๐Ÿ”ถ coverage
    class Topology.RelCWComplex.FiniteType {X : Type u} [TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] :
    Prop

    A CW complex is of finite type if cell C n is finite for every n.

    Instances
      source
      ๐Ÿ”ถ coverage
      class Topology.RelCWComplex.Finite {X : Type u_1} [TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] extends Topology.RelCWComplex.FiniteDimensional C, Topology.RelCWComplex.FiniteType C :
      Prop

      A CW complex is finite if it is finite dimensional and of finite type.

      Instances
        source
        ๐Ÿ“ coverage
        theorem Topology.RelCWComplex.finite_of_finiteDimensional_finiteType {X : Type u_1} [TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] [FiniteDimensional C] [FiniteType C] :
        Finite C
        source
        ๐Ÿ”ธ coverage
        @[implicit_reducible]
        def Topology.RelCWComplex.mkFiniteType {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (disjointBase' : โˆ€ (n : โ„•) (i : cell n), Disjoint (โ†‘(map n i) '' Metric.ball 0 1) D) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (D โˆช โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (closed' : โˆ€ A โŠ† C, (โˆ€ (n : โ„•) (j : cell n), IsClosed (A โˆฉ โ†‘(map n j) '' Metric.closedBall 0 1)) โˆง IsClosed (A โˆฉ D) โ†’ IsClosed A) (isClosedBase : IsClosed D) (union' : D โˆช โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) :
        RelCWComplex C D

        If we want to construct a relative CW complex of finite type, we can add the condition finite_cell and relax the condition mapsTo.

        Instances For
          source
          ๐Ÿ“ coverage
          theorem Topology.RelCWComplex.mkFiniteType_map {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (disjointBase' : โˆ€ (n : โ„•) (i : cell n), Disjoint (โ†‘(map n i) '' Metric.ball 0 1) D) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (D โˆช โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (closed' : โˆ€ A โŠ† C, (โˆ€ (n : โ„•) (j : cell n), IsClosed (A โˆฉ โ†‘(map n j) '' Metric.closedBall 0 1)) โˆง IsClosed (A โˆฉ D) โ†’ IsClosed A) (isClosedBase : IsClosed D) (union' : D โˆช โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) (n : โ„•) (i : cell n) :
          RelCWComplex.map n i = map n i
          source
          ๐Ÿ“ coverage
          theorem Topology.RelCWComplex.mkFiniteType_cell {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (disjointBase' : โˆ€ (n : โ„•) (i : cell n), Disjoint (โ†‘(map n i) '' Metric.ball 0 1) D) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (D โˆช โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (closed' : โˆ€ A โŠ† C, (โˆ€ (n : โ„•) (j : cell n), IsClosed (A โˆฉ โ†‘(map n j) '' Metric.closedBall 0 1)) โˆง IsClosed (A โˆฉ D) โ†’ IsClosed A) (isClosedBase : IsClosed D) (union' : D โˆช โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) (n : โ„•) :
          RelCWComplex.cell C n = cell n
          source
          ๐Ÿ“ coverage
          theorem Topology.RelCWComplex.finiteType_mkFiniteType {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (disjointBase' : โˆ€ (n : โ„•) (i : cell n), Disjoint (โ†‘(map n i) '' Metric.ball 0 1) D) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (D โˆช โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (closed' : โˆ€ A โŠ† C, (โˆ€ (n : โ„•) (j : cell n), IsClosed (A โˆฉ โ†‘(map n j) '' Metric.closedBall 0 1)) โˆง IsClosed (A โˆฉ D) โ†’ IsClosed A) (isClosedBase : IsClosed D) (union' : D โˆช โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) :
          FiniteType C

          A CW complex that was constructed using RelCWComplex.mkFiniteType is of finite type.

          source
          ๐Ÿ”ธ coverage
          @[implicit_reducible]
          def Topology.CWComplex.mkFiniteType {X : Type u} [TopologicalSpace X] (C : Set X) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (closed' : โˆ€ A โŠ† C, (โˆ€ (n : โ„•) (j : cell n), IsClosed (A โˆฉ โ†‘(map n j) '' Metric.closedBall 0 1)) โ†’ IsClosed A) (union' : โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) :
          CWComplex C

          If we want to construct a CW complex of finite type, we can add the condition finite_cell and relax the condition mapsTo.

          Instances For
            source
            ๐Ÿ“ coverage
            theorem Topology.CWComplex.mkFiniteType_cell {X : Type u} [TopologicalSpace X] (C : Set X) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (closed' : โˆ€ A โŠ† C, (โˆ€ (n : โ„•) (j : cell n), IsClosed (A โˆฉ โ†‘(map n j) '' Metric.closedBall 0 1)) โ†’ IsClosed A) (union' : โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) (n : โ„•) :
            Topology.CWComplex.cell C n = cell n
            source
            ๐Ÿ“ coverage
            theorem Topology.CWComplex.mkFiniteType_map {X : Type u} [TopologicalSpace X] (C : Set X) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (closed' : โˆ€ A โŠ† C, (โˆ€ (n : โ„•) (j : cell n), IsClosed (A โˆฉ โ†‘(map n j) '' Metric.closedBall 0 1)) โ†’ IsClosed A) (union' : โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) (n : โ„•) (i : cell n) :
            Topology.CWComplex.map n i = map n i
            source
            ๐Ÿ“ coverage
            theorem Topology.CWComplex.finiteType_mkFiniteType {X : Type u} [TopologicalSpace X] (C : Set X) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (closed' : โˆ€ A โŠ† C, (โˆ€ (n : โ„•) (j : cell n), IsClosed (A โˆฉ โ†‘(map n j) '' Metric.closedBall 0 1)) โ†’ IsClosed A) (union' : โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) :
            FiniteType C

            A CW complex that was constructed using CWComplex.mkFiniteType is of finite type.

            source
            ๐Ÿ”ธ coverage
            @[implicit_reducible]
            def Topology.RelCWComplex.mkFinite {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (eventually_isEmpty_cell : โˆ€แถ  (n : โ„•) in Filter.atTop, IsEmpty (cell n)) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (disjointBase' : โˆ€ (n : โ„•) (i : cell n), Disjoint (โ†‘(map n i) '' Metric.ball 0 1) D) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (D โˆช โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (isClosedBase : IsClosed D) (union' : D โˆช โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) :
            RelCWComplex C D

            If we want to construct a finite relative CW complex we can add the conditions eventually_isEmpty_cell and finite_cell, relax the condition mapsTo and remove the condition closed'.

            Instances For
              source
              ๐Ÿ“ coverage
              theorem Topology.RelCWComplex.mkFinite_map {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (eventually_isEmpty_cell : โˆ€แถ  (n : โ„•) in Filter.atTop, IsEmpty (cell n)) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (disjointBase' : โˆ€ (n : โ„•) (i : cell n), Disjoint (โ†‘(map n i) '' Metric.ball 0 1) D) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (D โˆช โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (isClosedBase : IsClosed D) (union' : D โˆช โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) (n : โ„•) (i : cell n) :
              RelCWComplex.map n i = map n i
              source
              ๐Ÿ“ coverage
              theorem Topology.RelCWComplex.mkFinite_cell {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (eventually_isEmpty_cell : โˆ€แถ  (n : โ„•) in Filter.atTop, IsEmpty (cell n)) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (disjointBase' : โˆ€ (n : โ„•) (i : cell n), Disjoint (โ†‘(map n i) '' Metric.ball 0 1) D) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (D โˆช โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (isClosedBase : IsClosed D) (union' : D โˆช โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) (n : โ„•) :
              RelCWComplex.cell C n = cell n
              source
              ๐Ÿ“ coverage
              theorem Topology.RelCWComplex.finite_mkFinite {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (eventually_isEmpty_cell : โˆ€แถ  (n : โ„•) in Filter.atTop, IsEmpty (cell n)) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (disjointBase' : โˆ€ (n : โ„•) (i : cell n), Disjoint (โ†‘(map n i) '' Metric.ball 0 1) D) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (D โˆช โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (isClosedBase : IsClosed D) (union' : D โˆช โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) :
              Finite C

              A CW complex that was constructed using RelCWComplex.mkFinite is finite.

              source
              ๐Ÿ”ธ coverage
              @[implicit_reducible]
              def Topology.CWComplex.mkFinite {X : Type u} [TopologicalSpace X] (C : Set X) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (eventually_isEmpty_cell : โˆ€แถ  (n : โ„•) in Filter.atTop, IsEmpty (cell n)) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (mapsTo_iff_image_subset : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (union' : โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) :
              CWComplex C

              If we want to construct a finite CW complex we can add the conditions eventually_isEmpty_cell and finite_cell, relax the condition mapsTo and remove the condition closed'.

              Instances For
                source
                ๐Ÿ“ coverage
                theorem Topology.CWComplex.mkFinite_cell {X : Type u} [TopologicalSpace X] (C : Set X) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (eventually_isEmpty_cell : โˆ€แถ  (n : โ„•) in Filter.atTop, IsEmpty (cell n)) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (mapsTo_iff_image_subset : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (union' : โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) (n : โ„•) :
                Topology.CWComplex.cell C n = RelCWComplex.cell C n
                source
                ๐Ÿ“ coverage
                theorem Topology.CWComplex.mkFinite_map {X : Type u} [TopologicalSpace X] (C : Set X) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (eventually_isEmpty_cell : โˆ€แถ  (n : โ„•) in Filter.atTop, IsEmpty (cell n)) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (mapsTo_iff_image_subset : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (union' : โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) (n : โ„•) (i : RelCWComplex.cell C n) :
                Topology.CWComplex.map n i = RelCWComplex.map n i
                source
                ๐Ÿ“ coverage
                theorem Topology.CWComplex.finite_mkFinite {X : Type u} [TopologicalSpace X] (C : Set X) (cell : โ„• โ†’ Type u) (map : (n : โ„•) โ†’ cell n โ†’ PartialEquiv (Fin n โ†’ โ„) X) (eventually_isEmpty_cell : โˆ€แถ  (n : โ„•) in Filter.atTop, IsEmpty (cell n)) (finite_cell : โˆ€ (n : โ„•), _root_.Finite (cell n)) (source_eq : โˆ€ (n : โ„•) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : โˆ€ (n : โ„•) (i : cell n), ContinuousOn (โ†‘(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : โ„•) ร— cell n) => โ†‘(map ni.fst ni.snd) '' Metric.ball 0 1) (mapsTo : โˆ€ (n : โ„•) (i : cell n), Set.MapsTo (โ†‘(map n i)) (Metric.sphere 0 1) (โ‹ƒ (m : โ„•), โ‹ƒ (_ : m < n), โ‹ƒ (j : cell m), โ†‘(map m j) '' Metric.closedBall 0 1)) (union' : โ‹ƒ (n : โ„•), โ‹ƒ (j : cell n), โ†‘(map n j) '' Metric.closedBall 0 1 = C) :
                Finite C

                A CW complex that was constructed using CWComplex.mkFinite is finite.

                source
                ๐Ÿ“ coverage
                theorem Topology.RelCWComplex.finite_of_finite_cells {X : Type u_2} [TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (finite : _root_.Finite ((n : โ„•) ร— cell C n)) :
                Finite C

                If the collection of all cells (of any dimension) of a relative CW complex C is finite, then C is finite as a CW complex.

                source
                ๐Ÿ“ coverage
                theorem Topology.RelCWComplex.finite_cells_of_finite {X : Type u_2} [TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [finite : Finite C] :
                _root_.Finite ((n : โ„•) ร— cell C n)

                If C is finite as a CW complex then the collection of all cells (of any dimension) is finite.

                source
                ๐Ÿ“ coverage
                theorem Topology.RelCWComplex.finite_iff_finite_cells {X : Type u_2} [TopologicalSpace X] {C D : Set X} [RelCWComplex C D] :
                Finite C โ†” _root_.Finite ((n : โ„•) ร— cell C n)

                A CW complex is finite iff the total number of its cells is finite.