map_id

Mathlib.Data.Multiset.MapFold

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

English

Mapping by the identity function leaves a multiset unchanged: map id s = s.

Русский

Отображение единичной функцией оставляет мультимножество без изменений: map id s = s.

LaTeX

$$$$ \\operatorname{map} id\, s = s $$$$

Lean4

theorem map_id (s : Multiset α) : map id s = s :=
  Quot.inductionOn s fun _l => congr_arg _ <| List.map_id _

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

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

Разделы

Аффилиация

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