image_preimage_inl_union_image_preimage_inr

English

For a set s ⊆ α ⊕ β, the image of Sum.inl on its preimage and the image of Sum.inr on its preimage together recreate s.

Русский

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

LaTeX

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

Lean4

theorem image_preimage_inl_union_image_preimage_inr (s : Set (α ⊕ β)) :
    Sum.inl '' (Sum.inl ⁻¹' s) ∪ Sum.inr '' (Sum.inr ⁻¹' s) = s := by
  rw [← preimage_sumElim, Sum.elim_inl_inr, preimage_id]

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