English
Principal (· + ·) o is equivalent to o = 0 or o ∈ { ω^k : k ∈ Ordinal }.
Русский
Принципиальность сложения для o эквивалентна тому, что либо o = 0, либо o принадлежит множеству { ω^k : k ∈ Ordinal }.
LaTeX
$$$Principal(\cdot + \cdot, o) \iff o = 0 \lor o \in \{ \omega^k : k \in \text{Ordinal} \}.$$$
Lean4
/-- The main characterization theorem for additive principal ordinals. -/
theorem principal_add_iff_zero_or_omega0_opow :
Principal (· + ·) o ↔ o = 0 ∨ o ∈ Set.range (ω ^ · : Ordinal → Ordinal) :=
by
rcases eq_or_ne o 0 with (rfl | ho)
· simp only [principal_zero, Or.inl]
· rw [principal_add_iff_add_left_eq_self]
simp only [ho, false_or]
refine
⟨fun H => ⟨_, ((lt_or_eq_of_le (opow_log_le_self _ ho)).resolve_left fun h => ?_)⟩, fun ⟨b, e⟩ =>
e.symm ▸ fun a => add_omega0_opow⟩
have := H _ h
have := lt_opow_succ_log_self one_lt_omega0 o
rw [opow_succ, lt_mul_iff_of_isSuccLimit isSuccLimit_omega0] at this
rcases this with ⟨a, ao, h'⟩
rcases lt_omega0.1 ao with ⟨n, rfl⟩
clear ao
revert h'
apply not_lt_of_ge
suffices e : ω ^ log ω o * n + o = o by simpa only [e] using le_add_right (ω ^ log ω o * ↑n) o
induction n with
| zero => simp [Nat.cast_zero, mul_zero, zero_add]
| succ n IH => simp only [Nat.cast_succ, mul_add_one, add_assoc, this, IH]
