image_toFinset — Mathlib

English

If α is decidable, then mapping a Finset of α through f and then converting back to Finset equals mapping the underlying multiset and converting back:

Русский

При наличииDecidableEq α выполняется равенство образа Finset на s.toFinset и отображение через map f затем toFinset совпадает с аналогичным преобразованием через s.map f.

LaTeX

$$$\\operatorname{image}(f, s^{\\mathrm{toFinset}}) = (s.map f)^{\\mathrm{toFinset}}$$$

Lean4

theorem image_toFinset [DecidableEq α] {s : Multiset α} : s.toFinset.image f = (s.map f).toFinset :=
  ext fun _ => by simp only [mem_image, Multiset.mem_toFinset, Multiset.mem_map]

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