closedCell_zero_eq_singleton — Mathlib

English

In a RelCWComplex, the 0-dimensional closed cell corresponding to a 0-cell j is a singleton consisting of the pointed map at j evaluated on the zero vector.

Русский

В RelCWComplex нулевая клетка, соответствующая нулевой клетке j, является синглтоном, состоящим из отображения map 0 j на нулевой вектор.

LaTeX

$$$\\text{closedCell}(0,j) = \\{(\\text{map } 0\\, j)(\\,\\emptyset\\,)\}$$$

Lean4

theorem closedCell_zero_eq_singleton [RelCWComplex C D] {j : cell C 0} : closedCell 0 j = {map 0 j ![]} := by
  simp [closedCell, Matrix.empty_eq]

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