cellFrontier_eq — Mathlib

English

CellFrontier on subcomplex equals the frontier on ambient: cellFrontier (C := E) n i = cellFrontier n (i : cell C n).

Русский

Граница клетки на подкомплексe равна границе клетки на окружающем.

LaTeX

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

Lean4

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

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