finite_subcomplex_of_finite — Mathlib

English

A subcomplex of a finite RelCWComplex is finite.

Русский

Подпоследовательность относительного CW-комплекса, являющаяся субкомплексом, конечна.

LaTeX

$$$\\text{finiteSubcomplex }(E)\\;\\text{for finite } C D$$$

Lean4

/-- A subcomplex of a finite CW complex is again finite. -/
instance finite_subcomplex_of_finite [T2Space X] [RelCWComplex C D] [Finite C] (E : Subcomplex C) :
    Finite (E : Set X) :=
  finite_of_finiteDimensional_finiteType _

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