le_iSup — Mathlib

English

For any small index set, the iSup is below a iff every index is below a.

Русский

Для любого малого индекса iSup f ≤ a эквивалентно ∀ i, f i ≤ a.

LaTeX

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

Lean4

/-- `le_ciSup` whenever the input type is small in the output universe. This lemma sometimes
fails to infer `f` in simple cases and needs it to be given explicitly. -/
protected theorem le_iSup {ι} (f : ι → Ordinal.{u}) [Small.{u} ι] : ∀ i, f i ≤ iSup f :=
  le_ciSup (bddAbove_of_small _)

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