max — Mathlib

English

Pointwise supremum of two antitone functions is antitone.

Русский

Пусть две антотонные функции, их точечный максимум антотонен.

LaTeX

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

Lean4

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

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