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

• RelCWComplex.FiniteDimensional: a CW complex is finite dimensional if it has only finitely many nonempty indexing types for the cells.
• RelCWComplex.FiniteType: a CW complex is of finite type if it has only finitely many cells in each dimension.
• RelCWComplex.Finite: a CW complex is finite if it is finite dimensional and of finite type.

Main statements

• RelCWComplex.mkFiniteType: if we want to construct a CW complex of finite type, we can relax the condition mapsTo.
• RelCWComplex.mkFinite: if we want to construct a finite CW complex, we can relax the condition mapsTo and can leave out the condition closed'.
• RelCWComplex.finite_iff_finite_cells: a CW complex is finite iff the total number of its cells is finite.

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.

• eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell C n)

  For some natural number n, the type cell C m is empty for all m ≥ n.

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.

• finite_cell (n : ℕ) : _root_.Finite (cell C n)

  cell C n is finite for every n.

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.

• eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell C n)
• finite_cell (n : ℕ) : _root_.Finite (cell C n)

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

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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.

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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.

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'.

Equations

• One or more equations did not get rendered due to their size.

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

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

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.

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'.

Equations

• One or more equations did not get rendered due to their size.

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

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

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.

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.

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.

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.