map_univ_coeEmbedding — Mathlib

English

The universal Finset of m, mapped by the coeEmbedding, yields the enumeration of m.

Русский

Все элементы m перечисляются через отображение coeEmbedding из универсального Finset.

LaTeX

$$(Finset.univ : Finset m).map m.coeEmbedding = m.toEnumFinset$$

Lean4

theorem map_univ_coeEmbedding (m : Multiset α) : (Finset.univ : Finset m).map m.coeEmbedding = m.toEnumFinset :=
  by
  ext ⟨x, i⟩
  simp only [Fin.exists_iff, Finset.mem_map, Finset.mem_univ, Multiset.coeEmbedding_apply, Prod.mk_inj,
    Multiset.exists_coe, Multiset.coe_mk, exists_prop, exists_eq_right_right, exists_eq_right,
    Multiset.mem_toEnumFinset, true_and]

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