English
If hp: 0 < f(0), then the function o ↦ veblenWith(f, o, 0) is normal.
Русский
При hp: 0 < f(0) функция o ↦ veblenWith(f, o, 0) является нормальной.
LaTeX
$$$\forall f:\,\operatorname{Ordinal} \to \operatorname{Ordinal},\ (0 < f(0)) \Rightarrow \operatorname{IsNormal}(o \mapsto \operatorname{veblenWith}(f,o,0))$$$
Lean4
theorem veblenWith_zero (hp : 0 < f 0) : IsNormal (veblenWith f · 0) :=
by
rw [isNormal_iff_strictMono_limit]
refine ⟨veblenWith_zero_strictMono hf hp, fun o ho a IH ↦ ?_⟩
rw [veblenWith_of_ne_zero f ho.ne_bot, derivFamily_zero]
apply nfpFamily_le fun l ↦ ?_
suffices ∃ b < o, List.foldr _ 0 l ≤ veblenWith f b 0
by
obtain ⟨b, hb, hb'⟩ := this
exact hb'.trans (IH b hb)
induction l with
| nil => use 0; simpa using ho.bot_lt
| cons a l IH =>
obtain ⟨b, hb, hb'⟩ := IH
refine
⟨_, ho.succ_lt (max_lt a.2 hb),
((veblenWith_right_strictMono hf _).monotone <|
hb'.trans <| veblenWith_left_monotone hf _ <| (le_max_right a.1 b).trans (le_succ _)).trans
?_⟩
rw [veblenWith_veblenWith_of_lt hf]
rw [lt_succ_iff]
exact le_max_left _ b
