image_union — Mathlib

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₂

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