openCell_eq — Mathlib

English

ClosedCell on subcomplex equals closedCell on ambient: closedCell(C := E) n i = closedCell n (i : cell C n).

Русский

Замкнутая клетка на подкомплексe равна замкнутой клетке на окружении: closedCell(C := E) n i = closedCell n (i : cell C n).

LaTeX

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

Lean4

@[simp]
theorem openCell_eq [T2Space X] [RelCWComplex C D] (E : Subcomplex C) (n : ℕ) (i : E.I n) :
    openCell (C := E) n i = openCell n (i : cell C n) := by rfl

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