inf — Mathlib

English

Pointwise supremum of two monotone functions is a monotone function.

Русский

Пусть f и g — монотонные функции на множестве; их точечное объединение по верхнему пределу тоже монотонно.

LaTeX

$$$ [Preorder α] [SemilatticeSup β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (f \sqcup g) s$$$

Lean4

/-- Pointwise infimum of two monotone functions is a monotone function. -/
protected theorem inf [Preorder α] [SemilatticeInf β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s)
    (hg : MonotoneOn g s) : MonotoneOn (f ⊓ g) s :=
  (hf.dual.sup hg.dual).dual

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