symmDiff_isCommutative

Mathlib.Order.SymmDiff

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

English

The symmetric difference is a commutative operation on α.

Русский

Симметрическая разность является коммутативной операцией на α.

LaTeX

$$$\\\\forall a,b \\\\in α, Std.Commutative (\\\\lambda x y, x \\\\Delta y)$$$

Lean4

instance symmDiff_isCommutative : Std.Commutative (α := α) (· ∆ ·) :=
  ⟨symmDiff_comm⟩

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

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

Разделы

Аффилиация

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