trans — Mathlib

English

The transitivity axiom holds: if a relates to b and b relates to c, then a relates to c in PreEnvelGroupRel.

Русский

Транзитивность: если a связано с b и b связано с c, то a связано с c.

LaTeX

$$$\forall a,b,c:\ PreEnvelGroupRel\ a\ b \Rightarrow PreEnvelGroupRel\ b\ c \Rightarrow PreEnvelGroupRel\ a\ c.$$$

Lean4

@[trans]
theorem trans {R : Type u} [Rack R] {a b c : PreEnvelGroup R} :
    PreEnvelGroupRel R a b → PreEnvelGroupRel R b c → PreEnvelGroupRel R a c
  | ⟨rab⟩, ⟨rbc⟩ => (rab.trans rbc).rel

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