finiteType_subcomplex_of_finiteType

English

If ambient C has finite type, then the underlying set of E has finite type as well: FiniteType C implies FiniteType (E:Set X).

Русский

Если C имеет конечный тип, то и подкомплекс E имеет конечный тип: FiniteType C ⇒ FiniteType (E:Set X).

LaTeX

$$FiniteType C$$

Lean4

instance finiteType_subcomplex_of_finiteType [T2Space X] [RelCWComplex C D] [FiniteType C] (E : Subcomplex C) :
    FiniteType (E : Set X) where
  finite_cell
    n :=
    let _ := FiniteType.finite_cell (C := C) (D := D) n
    Subtype.finite

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