toSingle₀Equiv_symm_apply_f_succ

English

For any f: C.X0 ⟶ X and any n, the (n+1)-th component of the inverse image under toSingle₀Equiv is 0.

Русский

Для любого f: C.X0 ⟶ X и любого n, (n+1)-ая компонента образа под обратным отображением toSingle₀Equiv равна 0.

LaTeX

$$$((\\mathrm{toSingle}_0^{\\mathrm{Equiv}} C X)^{-1} f)_{n+1} = 0$$$

Lean4

@[simp]
theorem toSingle₀Equiv_symm_apply_f_succ {C : CochainComplex V ℕ} {X : V} (f : C.X 0 ⟶ X) (n : ℕ) :
    ((toSingle₀Equiv C X).symm f).f (n + 1) = 0 := by rfl

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