lt_iSup_iff — Mathlib

English

Whenever the bound type is small, an inequality a < iSup f is equivalent to existence of i with a < f i.

Русский

Если источник мал, то a < iSup f эквивалентно существованию i с a < f i.

LaTeX

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

Lean4

/-- `lt_ciSup_iff'` whenever the input type is small in the output universe. -/
protected theorem lt_iSup_iff {ι} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u} ι] : a < iSup f ↔ ∃ i, a < f i :=
  lt_ciSup_iff'
    (bddAbove_of_small _)
      -- TODO: state in terms of `IsSuccLimit`.

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