image_insert — Mathlib

English

Image of an inserted element equals inserting its image: image f (insert a s) = insert (f a) (image f s).

Русский

Образ вставки элемента равен вставке его образа: image f (insert a s) = insert (f a) (image f s).

LaTeX

$$$\mathrm{image}\ f\ (\mathrm{insert}\ a\ s) = \mathrm{insert}\ (f(a))\ (\mathrm{image}\ f\ s)$$$

Lean4

@[simp]
theorem image_insert [DecidableEq α] (f : α → β) (a : α) (s : Finset α) :
    (insert a s).image f = insert (f a) (s.image f) := by grind

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