not_bddAbove_compl_of_small — Mathlib

English

If s is a small subset of nimbers, then its complement is not bounded above.

Русский

Если s — малое подмножество нимберов, то его дополнение не ограничено сверху.

LaTeX

$$$\\\\forall s\\\\subseteq \\\\mathrm{Nimber},\\\\ Small(s)\\\\Rightarrow \\\\neg \\\\exists M,\\\\forall x\\\\ (x\\\\in s^{\\\\complement}\\\\Rightarrow x\\\\le M).$$$

Lean4

theorem not_bddAbove_compl_of_small (s : Set Nimber.{u}) [Small.{u} s] : ¬BddAbove sᶜ :=
  Ordinal.not_bddAbove_compl_of_small s

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