range_inl_union_range_inr — Mathlib

English

Let α and β be types. The images of α under Sum.inl and of β under Sum.inr partition α ⊕ β; equivalently, every element of α ⊕ β lies in the image of inl or inr.

Русский

Пусть α и β – множества. Образы Sum.inl: α → α ⊕ β и Sum.inr: β → α ⊕ β_completely разбивают множество α ⊕ β: каждый элемент α ⊕ β равен inl a или inr b.

LaTeX

$$$\operatorname{range}(\mathrm{Sum.inl}) \cup \operatorname{range}(\mathrm{Sum.inr}) = \mathrm{univ}$$$

Lean4

@[simp]
theorem range_inl_union_range_inr : range (Sum.inl : α → α ⊕ β) ∪ range Sum.inr = univ :=
  isCompl_range_inl_range_inr.sup_eq_top

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