inf — Mathlib

English

The pointwise infimum of two monotone functions is monotone.

Русский

Пусть f,g монотонны; их точечный инфimum f ⊓ g монотонен.

LaTeX

$$$\text{Monotone.inf}\; (hf: Monotone f) (hg: Monotone g) : Monotone (f ⊓ g)$$$

Lean4

/-- Pointwise infimum of two monotone functions is a monotone function. -/
protected theorem inf [Preorder α] [SemilatticeInf β] {f g : α → β} (hf : Monotone f) (hg : Monotone g) :
    Monotone (f ⊓ g) := fun _ _ h => inf_le_inf (hf h) (hg h)

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