English
If f and g are strictly monotone, and p is a predicate with decidable truth, then the piecewise function defined by if p(x) then f(x) else g(x) is strictly monotone, under suitable hypotheses.
Русский
Если f и g строго монотонны и p — DecidablePred, то функция x ↦ if p(x) then f(x) else g(x) сохраняет строгую монотонность при подходящих условиях.
LaTeX
$$$\\forall {f g} \\; (hf: StrictMono f) (hg: StrictMono g) {p : \\alpha \\to \\text{Prop}} [\\text{DecidablePred } p]\\; (hp : \\forall {x y}, x < y \\to p y \\to p x) (hfg : \\forall x, f x \\le g x) \\; →\\; StrictMono (\\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 y⦄, p x → ¬p y → x < y → f x < g y) :
StrictMono fun x ↦ if p x then f x else g x := by
intro x y h
by_cases hy : p y
· have hx : p x := hp h hy
simpa [hx, hy] using hf h
by_cases hx : p x
· simpa [hx, hy] using hfg hx hy h
· simpa [hx, hy] using hg h
