singleMapHomologicalComplex_hom_app_ne

English

In the single-map construction, if the two indices i and j are distinct (i ≠ j), then the i-th component of the inverse map is zero.

Русский

В конструкции с одиночной картой, если индексы i и j различны (i ≠ j), то i-я компонента обратной карты равна нулю.

LaTeX

$$$\text{If } i \\neq j, \quad ((\mathrm{singleMapHomologicalComplex} F \ c \ j).\mathrm{hom}.\mathrm{app} \ X).f_i = 0.$$$

Lean4

@[simp]
theorem singleMapHomologicalComplex_hom_app_ne {i j : ι} (h : i ≠ j) (X : W₁) :
    ((singleMapHomologicalComplex F c j).hom.app X).f i = 0 := by simp [singleMapHomologicalComplex, h]

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