finite_iff_finite_cells — Mathlib

English

A RelCWComplex is finite iff the total number of its cells is finite.

Русский

RelCWComplex конечен тогда и только тогда, когда общее число клеток конечное.

LaTeX

$$$$ \\text{Finite}(C) \\iff \\operatorname{Finite}\\left(\\sum_{n} cell(C,n)\\right). $$$$

Lean4

/-- A CW complex is finite iff the total number of its cells is finite. -/
theorem finite_iff_finite_cells : Finite C ↔ _root_.Finite (Σ n, cell C n) :=
  ⟨fun h ↦ finite_cells_of_finite (finite := h), finite_of_finite_cells⟩

Похожие утверждения