pair_comm

Mathlib.Data.Multiset.ZeroCons

URI: https://scilib.ai/kg/mathlib#Multiset.pair_comm

English

The multiset of a pair {x, y} is equal to {y, x}.

Русский

Мультимножество пары {x, y} равно {y, x}.

LaTeX

$$$\\{x, y\\} = \\{y, x\\}$$$

Lean4

theorem pair_comm (x y : α) : ({ x, y } : Multiset α) = { y, x } :=
  cons_swap x y 0

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

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

Разделы

Аффилиация

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