max — Mathlib

English

If f and g are monotone functions from α to β, with α a preorder and β a semilattice inf, then the function x ↦ min(f(x), g(x)) is monotone.

Русский

Если f и g монотонны, то функция x ↦ min(f(x), g(x)) монотонна.

LaTeX

$$$ \text{Monotone}(f) \rightarrow \text{Monotone}(g) \rightarrow \text{Monotone}(x \mapsto \min(f(x), g(x))) $$$

Lean4

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

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