English
Decompose a dependent if-then-else into a supremum of two disjoint cases: sup_i (if p(i) then f(i,p(i)) else g(i,p(i))).
Русский
Разложение зависимого ветвления if-then-else в суперимпозицию двух случаев: sup_i (if p(i) then f(i,p(i)) else g(i,p(i))).
LaTeX
$$$\\\\bigvee_i \\\\bigl(\\\\text{if } p(i) \\text{ then } f(i,p(i)) \\text{ else } g(i,p(i))\\\\bigr) = \\\\max \\\\bigl( \\\\bigvee_i \\\\bigl( f(i, p(i)) \\bigr), \\\\bigl( \\\\bigvee_i \\\\bigl( g(i, \\, p(i)) \\bigr) \\\\bigr) \\\\bigr)$$$
Lean4
theorem iSup_dite (f : ∀ i, p i → α) (g : ∀ i, ¬p i → α) :
⨆ i, (if h : p i then f i h else g i h) = (⨆ (i) (h : p i), f i h) ⊔ ⨆ (i) (h : ¬p i), g i h :=
by
rw [← iSup_sup_eq]
congr 1 with i
split_ifs with h <;> simp [h]
