sInf — Mathlib

English

If a family {f_i} of functions f_i: α → β consists of monotone maps, then their pointwise infimum g(a) = inf_i f_i(a) is monotone in a.

Русский

Если семейство функций {f_i} с отображениями f_i: α → β состоит только из монотонных отображений, то их точечный инфимум g(a) = inf_i f_i(a) монотонен по a.

LaTeX

$$If ∀ i, f_i is Monotone, then Monotone( iInf_i f_i ).$$

Lean4

protected theorem sInf (hs : ∀ f ∈ s, Monotone f) : Monotone (sInf s) := fun _ _ h ↦ iInf_mono fun f ↦ hs f f.2 h

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