coe_orderIsoMultiset_symm

Mathlib.Data.Finsupp.Multiset

URI: https://scilib.ai/kg/mathlib#Finsupp.coe_orderIsoMultiset_symm

English

The inverse function of the order isomorphism equals Multiset.toFinsupp.

Русский

Обратная функция упорядоченного изоморфизма равна Multiset.toFinsupp.

LaTeX

$$$\bigl\langle\mathrm{orderIsoMultiset}^{-1}\bigr\rangle = \mathrm{toFinsupp}$$$

Lean4

@[simp]
theorem coe_orderIsoMultiset_symm [DecidableEq ι] : ⇑(@orderIsoMultiset ι).symm = Multiset.toFinsupp :=
  rfl

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

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

Разделы

Аффилиация

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