image2_union_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem image2_union_left : image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t := by
  simp_rw [← image_prod, union_prod, image_union]

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