flip_eq

Mathlib.Logic.OpClass

URI: https://scilib.ai/kg/mathlib#IsSymmOp.flip_eq

English

If an operation is symmetric, then flipping the arguments leaves the operation unchanged.

Русский

Если операция симметрична, то смена аргументов не меняет операцию.

LaTeX

$$$\forall {op}, [\text{IsSymmOp}(op)] \Rightarrow \text{flip}(op)=op$$$

Lean4

theorem flip_eq (op : α → α → β) [IsSymmOp op] : flip op = op :=
  funext fun a ↦ funext fun b ↦ (IsSymmOp.symm_op a b).symm

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

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

Разделы

Аффилиация

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