English
The image of a union equals the union of images: image f (s1 ∪ s2) = image f s1 ∪ image f s2.
Русский
Образ объединения равен объединению образов: image f (s1 ∪ s2) = image f s1 ∪ image f s2.
LaTeX
$$$\mathrm{image}\ f\ (s_1 \cup s_2) = \mathrm{image}\ f\ s_1 \cup \mathrm{image}\ f\ s_2$$$
Lean4
theorem image_union [DecidableEq α] {f : α → β} (s₁ s₂ : Finset α) : (s₁ ∪ s₂).image f = s₁.image f ∪ s₂.image f :=
mod_cast Set.image_union f s₁ s₂