Theorems · Theorem · field theory

Real.sSup_le

∀ {s : Set ℝ} {a : ℝ}, (∀ x ∈ s, x ≤ a) → 0 ≤ a → sSup s ≤ a

As sSup s = 0 when s is an empty set of reals, it suffices to show that all elements of s are at most some nonnegative number a to show that sSup s ≤ a. See also csSup_le.

Defined in

Mathlib.Algebra.Order.Archimedean.Real.Basic

Cited by

2 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound