coe_orderIsoMultiset

Mathlib.Data.Finsupp.Multiset

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

English

The function underlying the order isomorphism orderIsoMultiset is toMultiset.

Русский

Функция, лежащая в основе упорядоченного изоморфизма orderIsoMultiset, равна toMultiset.

LaTeX

$$$\bigl\langle\text{orderIsoMultiset}\bigr\rangle = \mathrm{toMultiset}$$$

Lean4

@[simp]
theorem coe_orderIsoMultiset [DecidableEq ι] : ⇑(@orderIsoMultiset ι _) = toMultiset :=
  rfl

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

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

Разделы

Аффилиация

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