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