map_union — Mathlib

English

Mapping distributes over Finset union: (s1 ∪ s2).map f = s1.map f ∪ s2.map f.

Русский

Образ объединения Finset под отображением распределяется: (s1 ∪ s2).map f = s1.map f ∪ s2.map f.

LaTeX

$$$ (s_1 \cup s_2).map f = s_1.map f \cup s_2.map f$$$

Lean4

theorem map_union [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α) :
    (s₁ ∪ s₂).map f = s₁.map f ∪ s₂.map f :=
  mod_cast Set.image_union f s₁ s₂

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