English
Let f: β ⊕ γ → α. Then the supremum over all inputs equals the supremum of the supremums over the left and right injections: ⨆x, f x = (⨆ i, f (inl i)) ⊔ (⨆ j, f (inr j)).
Русский
Пусть f: β ⊕ γ → α. Тогда наивысшая граница значения f по всем входам равна максимуму двух отдельных верхних границ: sup_{x} f(x) = sup_i f(inl i) ⊔ sup_j f(inr j).
LaTeX
$$$\\displaystyle \\big\\vee_{x} f(x) = \\big\\vee_{i} f(\\mathrm{inl}\\, i) \\;\\vee\\; \\big\\vee_{j} f(\\mathrm{inr}\\, j)$$$
Lean4
theorem iSup_sum {f : β ⊕ γ → α} : ⨆ x, f x = (⨆ i, f (Sum.inl i)) ⊔ ⨆ j, f (Sum.inr j) :=
eq_of_forall_ge_iff fun c => by simp only [sup_le_iff, iSup_le_iff, Sum.forall]
