Theorems · Theorem · field theory

Real.le_iInf

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

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 least some nonpositive number a to show that a ≤ ⨅ i, f i. See also le_ciInf.

Defined in

Mathlib.Algebra.Order.Archimedean.Real.Basic

Cited by

1 results in Mathlib

Foundations

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