English
If e,a are ONote with NF, and a' is an ordinal with e0: repr e ≠ 0, and a' < ω^{repr e}, then for any n ∈ ℕ+, we have ((ω^{repr e} · n) + a')^{ω} = (ω^{repr e})^{ω}.
Русский
Если e, a — ONote с NF, и a' — ординал с e0: repr e ≠ 0, а также a' < ω^{repr e}, то для любого n ∈ ℕ+ имеем ((ω^{repr e} · n) + a')^{ω} = (ω^{repr e})^{ω}.
LaTeX
$$$\\forall e\\,a\\,[NF\\ e][NF\\ a]\\;{a'}\\;\\big( e0 : repr\\, e \\neq 0 \\wedge a' < \\omega^{\\operatorname{repr} e} \\big) \\Rightarrow \\forall n\\,(n\\in\\mathbb{N}^+, )\\;\\left( (\\omega^{\\operatorname{repr} e} \\cdot n + a')^{\\omega} = (\\omega^{\\operatorname{repr} e})^{\\omega} \\right)$$$
Lean4
theorem repr_opow_aux₁ {e a} [Ne : NF e] [Na : NF a] {a' : Ordinal} (e0 : repr e ≠ 0)
(h : a' < (ω : Ordinal.{0}) ^ repr e) (aa : repr a = a') (n : ℕ+) :
((ω : Ordinal.{0}) ^ repr e * (n : ℕ) + a') ^ (ω : Ordinal.{0}) = (ω ^ repr e) ^ (ω : Ordinal.{0}) :=
by
subst aa
have No := Ne.oadd n (Na.below_of_lt' h)
have := omega0_le_oadd e n a
rw [repr] at this
refine le_antisymm ?_ (opow_le_opow_left _ this)
apply (opow_le_of_isSuccLimit ((opow_pos _ omega0_pos).trans_le this).ne' isSuccLimit_omega0).2
intro b l
have := (No.below_of_lt (lt_succ _)).repr_lt
rw [repr] at this
apply (opow_le_opow_left b <| this.le).trans
rw [← opow_mul, ← opow_mul]
apply opow_le_opow_right omega0_pos
rcases le_or_gt ω (repr e) with h | h
· apply (mul_le_mul_left' (le_succ b) _).trans
rw [← add_one_eq_succ, add_mul_succ _ (one_add_of_omega0_le h), add_one_eq_succ, succ_le_iff]
gcongr
exact isSuccLimit_omega0.succ_lt l
· apply (principal_mul_omega0 (isSuccLimit_omega0.succ_lt h) l).le.trans
simpa using mul_le_mul_right' (one_le_iff_ne_zero.2 e0) ω
