English
Let p and q be propositions and s: Or p q → α. Then iSup over x of s x equals the maximum of iSup over i with s(Or.inl i) and iSup over j with s(Or.inr j).
Русский
Пусть p и q — суждения, и s: Or p q → α. Тогда iSup по x равен максимуму из iSup по Or.inl и iSup по Or.inr.
LaTeX
$$$\\\\bigvee_{x} s(x) = \\\\max( \\\\bigvee_i s(\\\\mathrm{inl} i), \\\\bigvee_j s(\\\\mathrm{inr} j) )$$$
Lean4
theorem iSup_or {p q : Prop} {s : p ∨ q → α} : ⨆ x, s x = (⨆ i, s (Or.inl i)) ⊔ ⨆ j, s (Or.inr j) :=
le_antisymm
(iSup_le fun i =>
match i with
| Or.inl _ => le_sup_of_le_left <| le_iSup (fun _ => s _) _
| Or.inr _ => le_sup_of_le_right <| le_iSup (fun _ => s _) _)
(sup_le (iSup_comp_le _ _) (iSup_comp_le _ _))
