bihimp_isCommutative

Mathlib.Order.SymmDiff

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

English

For all a,b, bihimp a b = bihimp b a.

Русский

Для любых a,b: bihimp a b = bihimp b a.

LaTeX

$$$$ \\text{bihimp}(a,b) = \\text{bihimp}(b,a) $$$$

Lean4

instance bihimp_isCommutative : Std.Commutative (α := α) (· ⇔ ·) :=
  ⟨bihimp_comm⟩

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

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

Разделы

Аффилиация

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