iSup_le_iff — Mathlib

English

For small index types, a is less than iSup f iff there exists i with a < f i.

Русский

Для малого множества индексов: a < iSup f эквивалентно существованию i с a < f i.

LaTeX

$$$a < iSup f \iff \exists i, a < f i$$$

Lean4

/-- `ciSup_le_iff'` whenever the input type is small in the output universe. -/
protected theorem iSup_le_iff {ι} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u} ι] : iSup f ≤ a ↔ ∀ i, f i ≤ a :=
  ciSup_le_iff' (bddAbove_of_small _)

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