coe_reverse

Mathlib.Data.Multiset.Defs

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

English

For any list l, the multiset of its reverse equals the multiset of the original list.

Русский

Для любого списка l мультсет переворота равен мультсету исходного списка.

LaTeX

$$$(\\text{reverse}(l)\\;:\\mathcal{M}(\\alpha))=l$$$

Lean4

@[simp]
theorem coe_reverse (l : List α) : (reverse l : Multiset α) = l :=
  Quot.sound <| reverse_perm _

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

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

Разделы

Аффилиация

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