trans — Mathlib

English

If h1 is a Zigzag from j1 to j2 and h2 is a Zigzag from j2 to j3, then their composition is a Zigzag from j1 to j3.

Русский

Если h1 — Zigzag от j1 к j2, и h2 — Zigzag от j2 к j3, то их композиция — Zigzag от j1 к j3.

LaTeX

$$$\forall j_1 j_2 j_3\, (h_1 : Zigzag\ j_1 j_2) (h_2 : Zigzag\ j_2 j_3) \Rightarrow Zigzag\ j_1 j_3$$$

Lean4

@[trans]
theorem trans {j₁ j₂ j₃ : J} (h₁ : Zigzag j₁ j₂) (h₂ : Zigzag j₂ j₃) : Zigzag j₁ j₃ :=
  zigzag_equivalence.trans h₁ h₂

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