trans — Mathlib

English

If two objects are equivalent and the second is equivalent to a third, then the first is equivalent to the third.

Русский

Если два объекта эквивалентны и второй эквивалентен третьему, то первый эквивалентен третьему.

LaTeX

$$$\\\\forall x,y,z,\\\\ (x \\\\approx y) \\\\rightarrow (y \\\\approx z) \\\\rightarrow (x \\\\approx z)$$$

Lean4

@[trans]
protected theorem trans {x y z : PGame} : (x ≈ y) → (y ≈ z) → (x ≈ z) :=
  _root_.trans

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