English
If f is strictly anti-monotone and g is strictly anti-monotone, then the piecewise function with a predicate p is strictly anti-monotone under appropriate hypotheses.
Русский
Если f и g строго антимонотонны, то функция по условию p — строго антимонотонна при подходящих предпосылках.
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 y}, p x \\to \\lnot p y \\to x < y \\to g y < f x) \\rightarrow \\text{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, g x ≤ f x) : StrictAnti fun x ↦ if p x then f x else g x :=
(hf.ite' hg hp) fun _ y _ _ h ↦ (hfg y).trans_lt (hf h)
