preimage_union — Mathlib

English

The preimage of a union equals the union of preimages: f.preimage(s ∪ t) = f.preimage(s) ∪ f.preimage(t).

Русский

Предобраз объединения равен объединению предобразов: f.preimage(s ∪ t) = f.preimage(s) ∪ f.preimage(t).

LaTeX

$$$f.preimage(s \\cup t) = f.preimage(s) \\cup f.preimage(t)$$$

Lean4

theorem preimage_union (s t : Set β) : f.preimage (s ∪ t) = f.preimage s ∪ f.preimage t :=
  SetRel.preimage_union _ s t

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