English
If f and g are strictly anti-monotone, and p is a decidable predicate, then the piecewise function defined by if p(x) then f(x) else g(x) is strictly anti-monotone under suitable hypotheses.
Русский
Если f и g строго антимонотонны, и p — DecidablePred, то функция f x при p(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 < f x) \\; →\\; StrictAnti (\\lambda x, if p x then f x else g x)$$$
Lean4
protected theorem ite (hf : StrictMono f) (hg : StrictMono g) {p : α → Prop} [DecidablePred p]
(hp : ∀ ⦃x y⦄, x < y → p y → p x) (hfg : ∀ x, f x ≤ g x) : StrictMono fun x ↦ if p x then f x else g x :=
(hf.ite' hg hp) fun _ y _ _ h ↦ (hf h).trans_le (hfg y)
