sym2_toFinset — Mathlib

English

For any multiset m, taking the sym2 after converting to a Finset equals taking Finset.sym2 after converting the Sym2 of m to a Finset.

Русский

Для произвольной многоразмерной множества m выполнение sym2 после приведения к Finset равно приведения Sym2 m к Finset затем применению sym2.

LaTeX

$$$m^{\to\mathrm{Finset}}.\mathrm{sym2} = m.\mathrm{sym2}^{\to \mathrm{Finset}}$$$

Lean4

theorem sym2_toFinset [DecidableEq α] (m : Multiset α) : m.toFinset.sym2 = m.sym2.toFinset :=
  by
  ext z
  refine z.ind fun x y ↦ ?_
  simp only [mk_mem_sym2_iff, Multiset.mem_toFinset, Multiset.mk_mem_sym2_iff]

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