map_univ_coe — Mathlib

English

The multiset is recovered by mapping the universal Finset elements to α.

Русский

Перебор множества всех элементов m через отображение в α восстанавливает m.

LaTeX

$$(Finset.univ : Finset m).val.map (fun x : m ↦ (x : α)) = m$$

Lean4

@[simp]
theorem map_univ_coe (m : Multiset α) : (Finset.univ : Finset m).val.map (fun x : m ↦ (x : α)) = m :=
  by
  have := m.map_toEnumFinset_fst
  rw [← m.map_univ_coeEmbedding] at this
  simpa only [Finset.map_val, Multiset.coeEmbedding_apply, Multiset.map_map, Function.comp_apply] using this

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