image_union — Mathlib

English

For any R and sets s1, s2, the image of their union equals the union of their images: image R (s1 ∪ s2) = image R s1 ∪ image R s2.

Русский

Образ объединения равен объединению образов: image R (s1 ∪ s2) = image R s1 ∪ image R s2.

LaTeX

$$$\\forall (R : SetRel \\alpha \\beta) (s1 s2 : Set \\alpha),\\\\ image\\,R\\,(s1 \\cup s2) = image\\,R\\,s1 \\cup image\\,R\\,s2$$$

Lean4

theorem image_union : image R (s₁ ∪ s₂) = image R s₁ ∪ image R s₂ := by aesop

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