iSup_nonneg' — Mathlib

English

If there exists i with 0 ≤ f(i), then 0 ≤ ⨆ i, f(i).

Русский

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

LaTeX

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

Lean4

/-- As `⨆ i, f i = 0` when the real-valued function `f` is unbounded above,
it suffices to show that `f` takes a nonnegative value to show that `0 ≤ ⨆ i, f i`. -/
theorem iSup_nonneg' (hf : ∃ i, 0 ≤ f i) : 0 ≤ ⨆ i, f i :=
  sSup_nonneg' <| Set.exists_range_iff.2 hf

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