mapToComposableArrows_app_2 — Mathlib

English

The 2-nd component of the induced morphism equals the third component τ3 of φ.

Русский

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

LaTeX

$$$\big(\operatorname{mapToComposableArrows}(\varphi)\big)_2 = \varphi_3^{\tau}$$$

Lean4

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

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