fromSingle₀Equiv_symm_apply_f_succ

English

For any f: X ⟶ C.X0 and any n, the (n+1)st component of the inverse image under the symmetrized equivalence is zero; i.e., the higher components vanish.

Русский

Для произвольного f: X → C.X0 и любого n, (n+1)-ая компонента образа через симметричное отображение эквивалентности равна нулю; т.е. вышеупомянутые компоненты нулевые.

LaTeX

$$$\\bigl( (\\mathrm{fromSingle}_0^{\\mathrm{Equiv}} C X)^{-1} f \\bigr)_{n+1} = 0 \\quad\\text{for all } n\\in\\mathbb{N}$$$

Lean4

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

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