English
Let p be a decidable predicate on β and f, g be functions from β to α. The supremum of the pointwise ite-predicate equals the join of the two corresponding suprema over the p- and non-p-parts of s.
Русский
Пусть p — распознаваемое по β. Пусть f,g: β → α. Тогда вершина последовательности s, применяющая ite(p, f, g), равна объединению супремумов f над подмножеством p и g над подмножеством ¬p.
LaTeX
$$$\displaystyle (s.sup f) = (s.filter p).sup f \;\lor\; (s.filter(\lambda i. \neg p i)).sup g$$$
Lean4
theorem sup_ite (p : β → Prop) [DecidablePred p] :
(s.sup fun i => ite (p i) (f i) (g i)) = (s.filter p).sup f ⊔ (s.filter fun i => ¬p i).sup g :=
fold_ite _
