Mathlib Map

Theorems · Theorem · field theory

Real.iInf_nonneg

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

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 nonnegative to show that 0 ≤ ⨅ i, f i.

Defined in
Mathlib.Algebra.Order.Archimedean.Real.Basic
Cited by
3 results in Mathlib
Foundations
Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

schnirelmannDensity_nonneg · cited by 2schnirelmannDensity_nonnegMetric.le_glueDist_inl_inr · cited by 2Metric.le_glueDist_inl_inrENNReal.ofReal_iInf · cited by 0ENNReal.ofReal_iInfReal · cited by 25697RealiInf · cited by 1690iInfle_rfl · cited by 1558le_rflReal.le_iInf · cited by 1Real.le_iInfReal.iInf_nonnegCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Realstatement and proof · cited by 25,697
  • iInfstatement · cited by 1,690
  • le_rflproof · cited by 1,558
  • Real.le_iInfproof · cited by 1

Cited by3

Results whose statement or proof uses this declaration.