cons_swap

Mathlib.Data.Multiset.ZeroCons

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

English

For any a,b and s, a ::ₘ b ::ₘ s equals b ::ₘ a ::ₘ s.

Русский

Для любых a,b и s: a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s.

LaTeX

$$a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s$$

Lean4

theorem cons_swap (a b : α) (s : Multiset α) : a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s :=
  Quot.inductionOn s fun _ => Quotient.sound <| Perm.swap _ _ _

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

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

Разделы

Аффилиация

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