map_zero_mem_closedCell — Mathlib

English

In a RelCWComplex, the basepoint 0 of the cell map lies in the closed cell: map n i 0 ∈ closedCell n i.

Русский

В RelCWComplex базовая точка отображения клетки удовлетворяет map n i 0 ∈ closedCell n i.

LaTeX

$$$(\mathrm{map}\ n\ i).toFun\ 0 \in closedCell\ n\ i$$$

Lean4

theorem map_zero_mem_closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) : map n i 0 ∈ closedCell n i :=
  openCell_subset_closedCell _ _ (map_zero_mem_openCell _ _)

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