image2_union_right — Mathlib

English

The image2 of a union in the second argument distributes over union: image2 f S (T ∪ T') = image2 f S T ∪ image2 f S T'.

Русский

Образ image2 по объединению во втором аргументе распределяется по объединению: image2 f S (T ∪ T').

LaTeX

$$$$\\operatorname{image2} f S (T \\cup T') \\\\;= \\\\operatorname{image2} f S T \\\\cup \\\\operatorname{image2} f S T'.$$

Lean4

theorem image2_union_right : image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t' := by
  rw [← image2_swap, image2_union_left, image2_swap f, image2_swap f]

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