English
For s ⊆ α ⊕ β, the image of Sum.elim f g on s equals the union of the images of preimages under f and g.
Русский
Для множества s ⊆ α ⊕ β образ Sum.elim f g на s равен объединению образов предобразов через f и g.
LaTeX
$$$\operatorname{image}(\mathrm{Sum.elim} f g) s = f '' (\mathrm{Sum.inl}^{-1}' s) \cup g '' (\mathrm{Sum.inr}^{-1}' s)$$$
Lean4
theorem image_sumElim (s : Set (α ⊕ β)) (f : α → γ) (g : β → γ) :
Sum.elim f g '' s = f '' (Sum.inl ⁻¹' s) ∪ g '' (Sum.inr ⁻¹' s) :=
by
rw [← image_preimage_inl_union_image_preimage_inr s]
simp [image_union, image_image, preimage_image_preimage]