Theorems · Theorem · field theory

Real.le_sInf

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

As sInf s = 0 when s is an empty set of reals, it suffices to show that all elements of s are at least some nonpositive number a to show that a ≤ sInf s. See also le_csInf.

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