inl_compl_union_inr_compl — Mathlib

English

In the disjoint sum context, the union of the images of the complements equals the complement of the union of the originals.

Русский

В контексте дизъюнктивной суммы объединение образов дополнений равно дополнению объединения исходников.

LaTeX

$$$\mathrm{image}(\mathrm{Sum.inl}, s^{c}) \cup \mathrm{image}(\mathrm{Sum.inr}, t^{c}) = \left( \mathrm{image}(\mathrm{Sum.inl}, s) \cup \mathrm{image}(\mathrm{Sum.inr}, t) \right)^{c}$$$

Lean4

theorem inl_compl_union_inr_compl {s : Set α} {t : Set β} :
    Sum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s ∪ Sum.inr '' t)ᶜ :=
  by
  rw [compl_union]
  aesop

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