English
Let f be an embedding f: α → β and s a finite subset of α. If a ∉ s, then the image under f of the set obtained by adding a to s equals the set consisting of f(a) together with the image of s.
Русский
Пусть f: α → β — инъекция и s — конечное подмножество α. Пусть a ∉ s. Тогда образ множества s ∪ {a} под действием f равен множеству {f(a)} ∪ image_f(s).
LaTeX
$$$\\operatorname{image}(f, s \\cup \\{a\\}) = \\operatorname{image}(f, s) \\cup \\{f(a)\\}$ при $a \\notin s$, где $f$ — инъективное отображение.$$
Lean4
@[simp]
theorem map_cons (f : α ↪ β) (a : α) (s : Finset α) (ha : a ∉ s) :
(cons a s ha).map f = cons (f a) (s.map f) (by simpa using ha) :=
eq_of_veq <| Multiset.map_cons f a s.val
