bddAbove_iff_small — Mathlib

English

For a set of ordinals, being bounded above is equivalent to being small.

Русский

Для множества порядковых чисел существование верхней границы эквивалентно малости.

LaTeX

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

Lean4

theorem bddAbove_iff_small {s : Set Ordinal.{u}} : BddAbove s ↔ Small.{u} s :=
  ⟨fun ⟨a, h⟩ => small_subset <| show s ⊆ Iic a from fun _ hx => h hx, fun _ => bddAbove_of_small _⟩

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