English
If p is a predicate on β with decidable truth, then infimum over s of the piecewise-constructed function ite(p(i), f(i), g(i)) equals the infimum of the corresponding filtered individuals: (s.inf (fun i => ite (p i) (f i) (g i))) = (s.filter p).inf f ⊓ (s.filter (fun i => ¬ p i)).inf g.
Русский
Если p — предикат на β с решаемостью, то inf по s от функции, заданной как ite(p(i), f(i), g(i)), равен inf f по тем элементам, где p истинно, взятому и inf g по тем, где p ложно.
LaTeX
$$$ \text{inf}_{i \in s} \; (\text{ite} (p i) (f i) (g i)) = \big( \operatorname{inf}_{i \in s \text{ } p i} f(i) \big) \wedge \big( \operatorname{inf}_{i \in s, \neg p i} g(i) \big) $$$
Lean4
theorem inf_ite (p : β → Prop) [DecidablePred p] :
(s.inf fun i ↦ ite (p i) (f i) (g i)) = (s.filter p).inf f ⊓ (s.filter fun i ↦ ¬p i).inf g :=
fold_ite _
