coe_toList — Mathlib

English

Let s be a finite set (finset) of α. The multiset obtained by viewing the list of its elements as a Multiset α is exactly the underlying multiset representing s, i.e., (s.toList : Multiset α) = s.val.

Русский

Пусть s — конечное множество над α. Мультимножество элементов s, полученное путём преобразования списка элементов в Multiset α, равно исходному мультимножество s.val.

LaTeX

$$$ (s.toList : \mathrm{Multiset} \alpha) = s.\mathrm{val} $$$

Lean4

@[simp, norm_cast]
theorem coe_toList (s : Finset α) : (s.toList : Multiset α) = s.val :=
  s.val.coe_toList

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