English
If a < veblen o a, then veblen o a = ω^x iff invVeblen₁ x = o and invVeblen₂ x = a.
Русский
Если a < veblen o a, то veblen o a = ω^x тогда и только тогда, когда invVeblen₁ x = o и invVeblen₂ x = a.
LaTeX
$$$\mathrm{veblen}(o,a) = \omega^x \iff invVeblen_1 x = o \land invVeblen_2 x = a$$$
Lean4
theorem veblen_eq_opow_iff (h : a < veblen o a) : veblen o a = ω ^ x ↔ invVeblen₁ x = o ∧ invVeblen₂ x = a :=
by
refine ⟨?_, fun ⟨hx, ha⟩ ↦ ?_⟩
· obtain rfl | ho := eq_zero_or_pos o
· rw [veblen_zero] at h
have := invVeblen₁_of_lt_opow h
have := invVeblen₂_of_lt_opow h
aesop
· rw [← veblen_veblen_of_lt ho, veblen_zero_apply, opow_right_inj one_lt_omega0]
rintro rfl
simp [invVeblen₁_veblen h, invVeblen₂_veblen ho.ne' h]
· convert ← veblen_invVeblen₁_invVeblen₂ x
