iSup_le — Mathlib

English

If every i satisfies f(i) ≤ a and a ≥ 0, then ⨆ i, f(i) ≤ a.

Русский

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

LaTeX

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

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 at most some nonnegative number `a` to show that `⨆ i, f i ≤ a`.

See also `ciSup_le`. -/
protected theorem iSup_le (hf : ∀ i, f i ≤ a) (ha : 0 ≤ a) : ⨆ i, f i ≤ a :=
  Real.sSup_le (Set.forall_mem_range.2 hf) ha

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