instLeftCommutativeOfRightCommutative

English

Let f be a binary operation of the form f: β → α → β that is right-commutative; define g(x,y) = f(y,x). Then g is left-commutative, i.e. for all a,b,c we have g(g(a,b),c) = g(g(a,c),b).

Русский

Пусть функция f: β → α → β удовлетворяет правой коммутативности; определим g(x,y) = f(y,x). Тогда g лево-коммутативна: для любых a,b,c выполняется g(g(a,b),c) = g(g(a,c),b).

LaTeX

$$$\\text{RightCommutative}(f) \\Rightarrow \\text{LeftCommutative}(\\lambda x\,y.\\ f(y\,x))$$$

Lean4

instance {f : β → α → β} [h : RightCommutative f] : LeftCommutative (fun x y ↦ f y x) :=
  ⟨fun _ _ _ ↦ (h.right_comm _ _ _).symm⟩

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