max — Mathlib

English

Pointwise maximum of two monotone functions is monotone on a set.

Русский

Точечное максимум двух монотонных функций является монотонной на множестве функции.

LaTeX

$$$ [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => max (f x) (g x)) s$$$

Lean4

/-- Pointwise maximum of two monotone functions is a monotone function. -/
protected theorem max [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s)
    (hg : MonotoneOn g s) : MonotoneOn (fun x => max (f x) (g x)) s :=
  hf.sup hg

Похожие утверждения