map_toEnumFinset_fst

Mathlib.Data.Multiset.Fintype

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

← MathLib Explorer

English

The multiset of first components of m.toEnumFinset recovers m via map fst.

Русский

Мультимножество первых координат m.toEnumFinset восстанавливает m через map fst.

LaTeX

$$m.toEnumFinset.val.map \mathrm{Prod.fst} = m$$

Lean4

@[simp]
theorem map_toEnumFinset_fst (m : Multiset α) : m.toEnumFinset.val.map Prod.fst = m := by ext a;
  simp [count_map, ← Finset.filter_val, eq_comm (a := a)]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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