English
Let a, c be positive ordinals with c not exceeding a raised to the first infinite power, and let b be any ordinal. Then the fixed-point approximation under the operation x ↦ a · x evaluated at a^ω · b + c equals a^ω · succ(b).
Русский
Пусть а и с – положительные ординалы, причём c не превосходит a^ω, и пусть b – произвольный ординал. Тогда аппроксимация фиксированной точки под операцией x ↦ a · x, вычисленная в a^ω · b + c, равна a^ω · succ(b).
LaTeX
$$$ (0 < a) \wedge (0 < c) \wedge (c \\le a^\\omega) \\rightarrow nfp(a \\cdot \\cdot)(a^\\omega \\cdot b + c) = a^\\omega \\cdot \\mathrm{succ}(b) $$$
Lean4
theorem nfp_mul_opow_omega0_add {a c : Ordinal} (b) (ha : 0 < a) (hc : 0 < c) (hca : c ≤ a ^ ω) :
nfp (a * ·) (a ^ ω * b + c) = a ^ ω * succ b :=
by
apply le_antisymm
· apply nfp_le_fp (isNormal_mul_right ha).monotone
· rw [mul_succ]
apply add_le_add_left hca
· dsimp only; rw [← mul_assoc, ← opow_one_add, one_add_omega0]
· obtain ⟨d, hd⟩ := mul_eq_right_iff_opow_omega0_dvd.1 ((isNormal_mul_right ha).nfp_fp ((a ^ ω) * b + c))
rw [hd]
apply mul_le_mul_left'
have := le_nfp (a * ·) (a ^ ω * b + c)
rw [hd] at this
have := (add_lt_add_left hc (a ^ ω * b)).trans_le this
rw [add_zero, mul_lt_mul_iff_right₀ (opow_pos ω ha)] at this
rwa [succ_le_iff]
