csInf_le_csSup — Mathlib

English

If s is bounded below, above, and nonempty, then sInf s ≤ sSup s.

Русский

Если множество ограничено снизу и сверху и непусто, то sInf s ≤ sSup s.

LaTeX

$$$\forall s:\\text{Set }\alpha,\ BddBelow\ s → BddAbove\ s → s.Nonempty ↓ sInf s \le sSup s$$$

Lean4

/-- If a set is bounded below and above, and nonempty, its infimum is less than or equal to
its supremum. -/
theorem csInf_le_csSup (hb : BddBelow s) (ha : BddAbove s) (ne : s.Nonempty) : sInf s ≤ sSup s :=
  isGLB_le_isLUB (isGLB_csInf ne hb) (isLUB_csSup ne ha) ne

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