openCell_zero_eq_singleton — Mathlib

English

For RelCWComplex C D and j : cell C 0, the open cell of dimension 0 is exactly the singleton of the image of the zero vector: openCell 0 j = { (map 0 j).toFun vecEmpty }.

Русский

Для RelCWComplex C D и j ∈ cell C 0, открытая клетка размерности 0 равна единичному множеству: openCell 0 j = { (map 0 j).toFun vecEmpty }.

LaTeX

$$$openCell\ 0\ j = \{(map\ 0\ j).toFun\ vecEmpty\}$$$

Lean4

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

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