map_def — Mathlib

English

For a Subcomplex E of C, openCell on the subcomplex equals openCell on the ambient complex with i cast to cell C n.

Русский

Для подкомплекса E отображение openCell на подкомплексе совпадает с открытой клеткой на окружении через приведение i к клетке C n.

LaTeX

$$openCell (C := E) n i = openCell n (i : cell C n)$$

Lean4

@[simp]
theorem map_def [T2Space X] [CWComplex C] (E : Subcomplex C) (n : ℕ) (i : E.I n) :
    map (C := E) n i = map (C := C) n i :=
  rfl

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