iInf_le_iSup — Mathlib

English

For a nonempty index set ι and any function f: ι → α in a complete lattice, the infimum is always less than or equal to the supremum.

Русский

Для непустого индексового множества ι и любой функции f: ι → α в полной решётке инфиму́мум всегда не превосходит суперматематическую верхнюю грань.

LaTeX

$$$$\\inf_i f(i) \\le \\sup_i f(i).$$$$

Lean4

theorem iInf_le_iSup [Nonempty ι] : ⨅ i, f i ≤ ⨆ i, f i :=
  (iInf_le _ (Classical.arbitrary _)).trans <| le_iSup _ (Classical.arbitrary _)

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