of_inv_hom — Mathlib

English

If f21: j2 → j1 and f23: j2 → j3, then Zigzag j1 j3 holds as the concatenation of an inverse edge and a forward edge.

Русский

Если f21: j2 → j1 и f23: j2 → j3, то Zigzag j1 j3 образуется как конкатенация противоположного ребра и прямого ребра.

LaTeX

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

Lean4

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

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