image_val — Mathlib

English

The underlying multiset of image is the deduplicated mapped underlying multiset: val(image f s) = dedup (map f s.val).

Русский

Опорная мультисета образа равна дедуплицированной карте подмножеств: val(image f s) = dedup (map f s.val).

LaTeX

$$$\\mathrm{val}(\\operatorname{image}(f,s)) = \\operatorname{dedup}(s.\\mathrm{val} \\mapsto f)$$$

Lean4

@[simp]
theorem image_val (f : α → β) (s : Finset α) : (image f s).1 = (s.1.map f).dedup :=
  rfl

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