iSup_nonneg — Mathlib

English

If every i has 0 ≤ f(i), then 0 ≤ ⨆ i, f(i).

Русский

Если каждый i удовлетворяет 0 ≤ f(i), тогда 0 ≤ ⨆ i, f(i).

LaTeX

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

Lean4

/-- As `⨆ i, f i = 0` when the domain of the real-valued function `f` is empty or unbounded above,
it suffices to show that all values of `f` are nonnegative to show that `0 ≤ ⨆ i, f i`. -/
theorem iSup_nonneg (hf : ∀ i, 0 ≤ f i) : 0 ≤ ⨆ i, f i :=
  sSup_nonneg <| Set.forall_mem_range.2 hf

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