toType_noMax_of_succ_lt — Mathlib

English

If o is a succ-limit, then o.toType has no maximum element.

Русский

Пусть o является succ-пределом; тогда у типа o.toType нет максимального элемента.

LaTeX

$$$$ \forall o\ \big(\mathrm{IsSuccLimit}(o) \Rightarrow \mathrm{NoMaxOrder}(o.\mathrm{toType})\big) $$$$

Lean4

theorem toType_noMax_of_succ_lt {o : Ordinal} (ho : ∀ a < o, succ a < o) : NoMaxOrder o.toType :=
  ⟨has_succ_of_type_succ_lt (type_toType _ ▸ ho)⟩

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