English
If the relative CW complex C D is finite, then the total number of cells Σ n, cell C n is finite.
Русский
Если RelCWComplex C D конечен, тогда суммарное число клеток Σ n, cell C n конечно.
LaTeX
$$$$ \\text{Finite}(C) \\Rightarrow \\operatorname{Finite}\\left(\\sum_{n} cell(C,n)\\right). $$$$
Lean4
/-- If `C` is finite as a CW complex then the collection of all cells (of any dimension) is
finite. -/
theorem finite_cells_of_finite [finite : Finite C] : _root_.Finite (Σ n, cell C n) := by
-- We show that there is a bijection between `Σ n, cell C n` and
-- `Σ (m : {m : ℕ // m < n}), cell C m`.
have h := finite.eventually_isEmpty_cell
have _ := finite.finite_cell
simp only [Filter.eventually_atTop, ge_iff_le] at h
rcases h with ⟨n, hn⟩
have (m) (j : cell C m) : m < n := by
by_contra h
exact (hn m (not_lt.1 h)).false j
let f : (Σ (m : { m : ℕ // m < n }), cell C m) ≃ Σ m, cell C m :=
{ toFun := fun ⟨m, j⟩ ↦ ⟨m, j⟩
invFun := fun ⟨m, j⟩ ↦ ⟨⟨m, this m j⟩, j⟩
left_inv := by simp [Function.LeftInverse]
right_inv := by simp [Function.RightInverse, Function.LeftInverse] }
rw [← Equiv.finite_iff f]
exact Finite.instSigma
