mapToComposableArrows_app_1 — Mathlib

English

The 1-st component of the induced morphism equals the second component τ2 of φ.

Русский

1-я компонента индуцированного морфизма равна второй компоненте τ2 φ.

LaTeX

$$$\big(\operatorname{mapToComposableArrows}(\varphi)\big)_1 = \varphi_2^{\tau}$$$

Lean4

@[simp]
theorem mapToComposableArrows_app_1 {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) :
    (ShortComplex.mapToComposableArrows φ).app 1 = φ.τ₂ :=
  rfl

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