act_self_act_eq — Mathlib

English

For all x,y in a unital shelf S, x acts on (x acts on y) equals x acts on y: x ◃ (x ◃ y) = x ◃ y.

Русский

Пусть S — унитальная полка. Для всех x,y выполняется x ◃ (x ◃ y) = x ◃ y.

LaTeX

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

Lean4

theorem act_self_act_eq (x y : S) : x ◃ (x ◃ y) = x ◃ y :=
  by
  have h : x ◃ (x ◃ y) = (x ◃ 1) ◃ (x ◃ y) := by rw [act_one]
  rw [h, ← Shelf.self_distrib, one_act]

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