iInf_nonneg — Mathlib

English

If every i, f(i) ≥ 0, then 0 ≤ iInf f.

Русский

Если каждый элемент функции неотрицателен, то 0 ≤ infimum.

LaTeX

$$$\\forall i, 0 \\le f(i) \\Rightarrow 0 \\le \\inf_{i} f(i)$$$

Lean4

/-- 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`. -/
theorem iInf_nonneg (hf : ∀ i, 0 ≤ f i) : 0 ≤ iInf f :=
  Real.le_iInf hf le_rfl

Похожие утверждения