sInf_le_sSup — Mathlib

English

For any s with lower and upper bounds, sInf(s) ≤ sSup(s).

Русский

Для множества s с нижней и верхней границами выполняется sInf(s) ≤ sSup(s).

LaTeX

$$$\\forall s, \\text{BddBelow}(s) \\land \\text{BddAbove}(s) \\Rightarrow \\operatorname{sInf}(s) \\le \\operatorname{sSup}(s)$$$

Lean4

theorem sInf_le_sSup (s : Set ℝ) (h₁ : BddBelow s) (h₂ : BddAbove s) : sInf s ≤ sSup s :=
  by
  rcases s.eq_empty_or_nonempty with (rfl | hne)
  · rw [sInf_empty, sSup_empty]
  · exact csInf_le_csSup h₁ h₂ hne

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