image_val_of_injOn — Mathlib

English

If f is injective on s, then the underlying multiset of image equals the map of s’s underlying multiset: (image f s).val = s.val.map f

Русский

Если f инъективна на s, то образ имеет достаточно свойства: val(image f s) = map f s.val (с дедупликацией внутри образа).

LaTeX

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

Lean4

theorem image_val_of_injOn (H : Set.InjOn f s) : (image f s).1 = s.1.map f :=
  (s.2.map_on H).dedup

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