biInf_le_biSup — Mathlib

English

If s is nonempty, then the infimum over i ∈ s of f i is less than or equal to the supremum over i ∈ s of f i.

Русский

Если s непусто, то инфимум по i∈s f(i) не превосходит супремум по i∈s f(i).

LaTeX

$$$ \\inf_{i \\in s} f(i) \\le \\sup_{i \\in s} f(i). $$$

Lean4

theorem biInf_le_biSup {ι : Type*} {s : Set ι} (hs : s.Nonempty) {f : ι → α} : ⨅ i ∈ s, f i ≤ ⨆ i ∈ s, f i :=
  (biInf_le _ hs.choose_spec).trans <| le_biSup _ hs.choose_spec

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