toSingle₀Equiv_symm_apply_f_zero

English

In the Nat-indexed setting, the 0th component of the inverse image under toSingle₀Equiv is f.

Русский

В настройке с индексами по Нат, 0-я компонента образа через toSingle₀Equiv равна f.

LaTeX

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

Lean4

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

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