not_bddAbove_principal — Mathlib

English

For any binary operation on ordinals, the set of ordinals o for which o is principal with respect to that operation is not bounded above.

Русский

Для произвольной бинарной операции над ординалами множество ординалов o, для которых o является принципиальным относительно этой операции, не имеет верхней границы.

LaTeX

$$$\neg \exists M \in \mathrm{Ord}, \forall o \,(Principal(op, o) \rightarrow o \le M).$$$

Lean4

/-- Principal ordinals under any operation are unbounded. -/
theorem not_bddAbove_principal (op : Ordinal → Ordinal → Ordinal) : ¬BddAbove {o | Principal op o} :=
  by
  rintro ⟨a, ha⟩
  exact ((le_nfp _ _).trans (ha (principal_nfp_iSup op (succ a)))).not_gt (lt_succ a)

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