map_union — Mathlib

English

For an injective function f, the image of the union equals the union of the images: map f (s ∪ t) = map f s ∪ map f t.

Русский

Для инъективной функции f образ объединения равен объединению образов: map f (s ∪ t) = map f s ∪ map f t.

LaTeX

$$$\\text{map } f (s \\cup t) = \\text{map } f s \\cup \\text{map } f t\\quad\\text{for } f \\text{ injective}.$$

Lean4

@[simp]
theorem map_union [DecidableEq β] {f : α → β} (finj : Function.Injective f) {s t : Multiset α} :
    map f (s ∪ t) = map f s ∪ map f t :=
  Quotient.inductionOn₂ s t fun l₁ l₂ => congr_arg ofList (by rw [List.map_append, List.map_diff finj])

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