finite_of_finiteDimensional_finiteType

English

If a RelCWComplex has finite-dimensional cells and satisfies the conditions of finite type, then it is of finite type, i.e., there exists a finite description of its cells and maps yielding a RelCWComplex.

Русский

Если RelCWComplex имеет конечного размера клетки и удовлетворяет условиям конечного типа, то он конечного типа: существует конечное описание его клеток и отображений, задающее RelCWComplex.

LaTeX

$$$$ \\text{FiniteType}(C) \\;\\Longleftarrow\\; \\text{finiteDimensional}(C) \\,\\land\\; \\text{finiteTypeConditions}(C,D,\\dots). $$$$

Lean4

theorem finite_of_finiteDimensional_finiteType [FiniteDimensional C] [FiniteType C] : Finite C
    where
  eventually_isEmpty_cell := FiniteDimensional.eventually_isEmpty_cell
  finite_cell n := FiniteType.finite_cell n

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