iSup_le_iff — Mathlib

English

For any f : ι → α, iSup f ≤ a if and only if f i ≤ a for all i.

Русский

Для любой f : ι → α справедливо: iSup f ≤ a тогда же и только тогда, когда f(i) ≤ a для всех i.

LaTeX

$$$\\\\forall {f : ι \\\\to α} {a : α}, \\\\left( iSup f \\\\le a \\\\right) \\\\Leftrightarrow \\\\forall i, f(i) \\\\le a$$$

Lean4

@[simp]
theorem iSup_le_iff : iSup f ≤ a ↔ ∀ i, f i ≤ a :=
  (isLUB_le_iff isLUB_iSup).trans forall_mem_range

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