ciInf_le_ciSup — Mathlib

English

If the range is bounded below and above, then iInf f ≤ iSup f.

Русский

Если диапазон значений f ограничен снизу и сверху, то iInf f ≤ iSup f.

LaTeX

$$BddBelow (Set.range f) → BddAbove (Set.range f) → iInf (fun i => f i) ≤ iSup (fun i => f i)$$

Lean4

theorem ciInf_le_ciSup [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) (hf' : BddAbove (range f)) :
    ⨅ i, f i ≤ ⨆ i, f i :=
  (ciInf_le hf (Classical.arbitrary _)).trans <| le_ciSup hf' (Classical.arbitrary _)

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