not_bddAbove_compl_of_small — Mathlib

English

For any small set s of ordinals, the complement sᶜ is not bounded above after lifting to ordinals, i.e., sᶜ has no upper bound.

Русский

Для любого малого множества ординалов дополнение к нему не ограничено сверху.

LaTeX

$$$\\forall s\\, [Small\\ s],\\; \\neg BddAbove\\, s^{\\complement}$$$

Lean4

theorem not_bddAbove_compl_of_small (s : Set Ordinal.{u}) [hs : Small.{u} s] : ¬BddAbove sᶜ :=
  by
  rw [bddAbove_iff_small]
  intro h
  have := small_union s sᶜ
  rw [union_compl_self, small_univ_iff] at this
  exact not_small_ordinal this

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