bddAbove_range — Mathlib

English

Small is equivalent to bounded above for sets of ordinals.

Русский

Малость эквивалентна ограниченности сверху для множеств порядковых чисел.

LaTeX

$$$BddAbove(s) \iff Small(s)$$$

Lean4

/-- The range of an indexed ordinal function, whose outputs live in a higher universe than the
    inputs, is always bounded above. See `Ordinal.lsub` for an explicit bound. -/
theorem bddAbove_range {ι : Type u} (f : ι → Ordinal.{max u v}) : BddAbove (Set.range f) :=
  ⟨(iSup (succ ∘ card ∘ f)).ord, by
    rintro a ⟨i, rfl⟩
    exact le_of_lt (Cardinal.lt_ord.2 ((lt_succ _).trans_le (le_ciSup (Cardinal.bddAbove_range _) _)))⟩

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