of_hom_hom — Mathlib

English

If f12: j1 → j2 and f23: j2 → j3, then Zigzag j1 j3 via the composition of the corresponding Zigzag steps.

Русский

Если f12: j1 → j2 и f23: j2 → j3, то Zigzag j1 j3 получаем через композицию шагов.

LaTeX

$$$\forall j_1 j_2 j_3\, (f_{12}: j_1 \to j_2) (f_{23}: j_2 \to j_3) \Rightarrow Zigzag\ j_1 j_3$$$

Lean4

theorem of_hom_hom {j₁ j₂ j₃ : J} (f₁₂ : j₁ ⟶ j₂) (f₂₃ : j₂ ⟶ j₃) : Zigzag j₁ j₃ :=
  (of_hom f₁₂).trans (of_hom f₂₃)

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