English
If f and g are strictly anti-monotone, then the function x ↦ if p(x) then f(x) else g(x) is strictly anti-monotone under suitable hypotheses.
Русский
Если f и g строго антимонотонны, то функция x ↦ если p(x) тогда f(x) иначе g(x) строго антимонотонна при подходящих условиях.
LaTeX
$$$\\forall {f g} \\; (hf: StrictAnti f) (hg: StrictAnti g) {p : \\alpha \\to \\text{Prop}} [\\text{DecidablePred } p]\\; (hp : \\forall {x y}, x < y \\to p y \\to p x) (hfg : \\forall x, g x \\le f x) \\; →\\; StrictAnti (\\lambda x, if p x then f x else g x)$$$
Lean4
protected theorem ite' (hf : StrictAnti f) (hg : StrictAnti g) {p : α → Prop} [DecidablePred p]
(hp : ∀ ⦃x y⦄, x < y → p y → p x) (hfg : ∀ ⦃x y⦄, p x → ¬p y → x < y → g y < f x) :
StrictAnti fun x ↦ if p x then f x else g x :=
StrictMono.ite' hf.dual_right hg.dual_right hp hfg
