singleMapHomologicalComplex_inv_app_ne

English

For i ≠ j, the i-th component of the inverse map at X vanishes.

Русский

Для i ≠ j i-я компонента в обратном отображении на X равна нулю.

LaTeX

$$$\forall i\,\forall j\, (i \neq j) \Rightarrow ((\mathrm{singleMapHomologicalComplex} F \ c \ j).\mathrm{inv}.\mathrm{app} X).f_i = 0$$$

Lean4

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

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