iSup_nonpos — Mathlib

English

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

Русский

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

LaTeX

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

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 nonpositive to show that `⨆ i, f i ≤ 0`. -/
theorem iSup_nonpos (hf : ∀ i, f i ≤ 0) : ⨆ i, f i ≤ 0 :=
  Real.iSup_le hf le_rfl

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