finiteDimensional_subcomplex_of_finiteDimensional

English

If ambient C is finite dimensional, then the subcomplex E is finite dimensional as well.

Русский

Если C конечномерен, то и подкомплекс E конечномерный.

LaTeX

$$FiniteDimensional (E : Set X)$$

Lean4

instance finiteDimensional_subcomplex_of_finiteDimensional [T2Space X] [RelCWComplex C D] [FiniteDimensional C]
    (E : Subcomplex C) : FiniteDimensional (E : Set X) where
  eventually_isEmpty_cell :=
    by
    filter_upwards [FiniteDimensional.eventually_isEmpty_cell (C := C) (D := D)] with n hn
    simp [isEmpty_subtype]

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