instRightCommutativeOfLeftCommutative

Mathlib.Logic.OpClass

URI: https://scilib.ai/kg/mathlib#instRightCommutativeOfLeftCommutative

English

If f is left-commutative, then the function y ↦ f(y, x) is right-commutative.

Русский

Если f лево-сопряжена, то функция (x,y) ↦ f(y,x) праволиневая.

LaTeX

$$$[\text{LeftCommutative}(f)] \Rightarrow \text{RightCommutative}(\lambda x y \mapsto f\,y\,x)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru