isSuccLimit_of_principal_add — Mathlib

English

If 1 < o and o is principal for addition, then o is a successor-limit ordinal.

Русский

Если o > 1 и o является принципиальным для сложения, то o является предельным следующим (пределом).

LaTeX

$$$(1 < o) \wedge Principal(+, o) \Rightarrow IsSuccLimit(o).$$$

Lean4

theorem isSuccLimit_of_principal_add (ho₁ : 1 < o) (ho : Principal (· + ·) o) : IsSuccLimit o :=
  by
  rw [isSuccLimit_iff, isSuccPrelimit_iff_succ_lt]
  exact ⟨ho₁.ne_bot, fun _ ha ↦ ho ha ho₁⟩

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