Theorems · Theorem · field theory

Real.iSup_le

∀ {ι : Sort u_1} {f : ι → ℝ} {a : ℝ}, (∀ (i : ι), f i ≤ a) → 0 ≤ a → ⨆ i, f i ≤ a

As ⨆ i, f i = 0 when the domain of the real-valued function f is empty, it suffices to show that all values of f are at most some nonnegative number a to show that ⨆ i, f i ≤ a. See also ciSup_le.

Defined in

Mathlib.Algebra.Order.Archimedean.Real.Basic

Cited by

4 results in Mathlib

Foundations

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