assoc — Mathlib

English

For all x,y,z in a unital shelf S, (x ◃ y) ◃ z = x ◃ (y ◃ z).

Русский

Для любых x,y,z в унитальной полке выполняется (x ◃ y) ◃ z = x ◃ (y ◃ z).

LaTeX

$$$(x \triangleleft y) \triangleleft z = x \triangleleft (y \triangleleft z)$$$

Lean4

/-- The associativity of a unital shelf comes for free.
-/
theorem assoc (x y z : S) : (x ◃ y) ◃ z = x ◃ y ◃ z := by
  rw [self_distrib, self_distrib, act_act_self_eq, act_self_act_eq]

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