image_sumElim — Mathlib

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]

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