of_hom_inv — Mathlib

English

If f12: j1 → j2 and f23: j3 → j2, then Zigzag j1 j3 holds via the combination of a direct edge and an inverse edge.

Русский

Если f12: j1 → j2 и f23: j3 → j2, то Zigzag j1 j3 существует через сочетание прямого и обратного рёбер.

LaTeX

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

Lean4

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

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