toFinset_cons — Mathlib

English

The toFinset of a cons node is the insert of its head into the toFinset of the tail.

Русский

toFinset для конструкции cons равна вставке головы элемента в toFinset хвоста.

LaTeX

$$$\\operatorname{toFinset}(a ::_m s) = \\operatorname{insert} a (\\operatorname{toFinset} s).$$$

Lean4

@[simp]
theorem toFinset_cons (a : α) (s : Multiset α) : toFinset (a ::ₘ s) = insert a (toFinset s) :=
  Finset.eq_of_veq dedup_cons

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