preimage_union — Mathlib

English

For any R and sets t1, t2, the preimage of their union equals the union of their preimages: preimage R (t1 ∪ t2) = preimage R t1 ∪ preimage R t2.

Русский

Предобраз объединения равен объединению предобразов: preimage R (t1 ∪ t2) = preimage R t1 ∪ preimage R t2.

LaTeX

$$$\\forall (R : SetRel \\alpha \\beta) (t1 t2 : Set \\beta),\\\\ preimage\\,R\\,(t1 \\cup t2) = preimage\\,R\\,t1 \\cup preimage\\,R\\,t2$$$

Lean4

theorem preimage_union : preimage R (t₁ ∪ t₂) = preimage R t₁ ∪ preimage R t₂ := by aesop

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