preimage_sumElim — Mathlib

English

For any sets s ⊆ α ⊕ β, the preimage under Sum.elim of s equals the union of the left and right preimages: Sum.inl '' (f ⁻¹' s) ∪ Sum.inr '' (g ⁻¹' s).

Русский

Для любого множества s ⊆ α ⊕ β предобраз Sum.elim f g на s равно объединению образов f на предобраз inl(s) и g на предобраз inr(s).

LaTeX

$$$\mathrm{Sum.elim} f g'' s = \mathrm{Sum.inl} '' (f^{-1}' s) \cup \mathrm{Sum.inr} '' (g^{-1}' s)$$$

Lean4

theorem preimage_sumElim (s : Set γ) (f : α → γ) (g : β → γ) :
    Sum.elim f g ⁻¹' s = Sum.inl '' (f ⁻¹' s) ∪ Sum.inr '' (g ⁻¹' s) := by ext (_ | _) <;> simp

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