min — Mathlib

English

Pointwise minimum of two antitone functions is antitone.

Русский

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

LaTeX

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

Lean4

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

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