English
The comparison between veblenWith f o1 a and veblenWith f o2 b is given by a standard three-way rule depending on the comparison of o1 and o2.
Русский
Сравнение между veblenWith f o1 a и veblenWith f o2 b задаётся трёхчастным правилом в зависимости от сравнения o1 и o2.
LaTeX
$$$\forall f:\,\operatorname{Ordinal} \to \operatorname{Ordinal},\ o1,o2,a,b:\operatorname{Ordinal},\ \operatorname{IsNormal}(f)\Rightarrow \operatorname{cmp}(\operatorname{veblenWith}(f,o1,a),\operatorname{veblenWith}(f,o2,b)) =\rightleftharpoons\begin{cases} \operatorname{cmp}(a,b) & \text{if } o1=o2, \\ \operatorname{cmp}(a,\operatorname{veblenWith}(f,o2,b)) & \text{if } o1o2. \end{cases}$$$
Lean4
theorem cmp_veblenWith :
cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
match cmp o₁ o₂ with
| .eq => cmp a b
| .lt => cmp a (veblenWith f o₂ b)
| .gt => cmp (veblenWith f o₁ a) b :=
by
obtain h | rfl | h := lt_trichotomy o₁ o₂
on_goal 2 => simp [(veblenWith_right_strictMono hf _).cmp_map_eq]
all_goals
conv_lhs => rw [← veblenWith_veblenWith_of_lt hf h]
simp [h.cmp_eq_lt, h.cmp_eq_gt, (veblenWith_right_strictMono hf _).cmp_map_eq]
