English
For any o and x, ω^x belongs to the range of veblen o if and only if o ≤ invVeblen₁ x.
Русский
Пусть o и x — ординалы. Тогда ω^x принадлежит диапазону функции veblen(o, ·) тогда и только тогда, когда o ≤ invVeblen₁ x.
LaTeX
$$$\omega^x \in \mathrm{range}(\mathrm{veblen}(o)) \iff o \le \mathrm{invVeblen}_1 x$$$
Lean4
theorem mem_range_veblen_iff_le_invVeblen₁ : ω ^ x ∈ range (veblen o) ↔ o ≤ invVeblen₁ x :=
by
obtain h | rfl | h := lt_trichotomy o (invVeblen₁ x)
· exact iff_of_true ⟨_, veblen_opow_eq_opow_iff.2 <| veblen_eq_of_lt_invVeblen₁ h⟩ h.le
· apply iff_of_true _ le_rfl
by_cases h : invVeblen₁ x = 0
· simp [h]
· simp_rw [mem_range_veblen h, veblen_opow_eq_opow_iff]
exact fun o ↦ veblen_eq_of_lt_invVeblen₁
· apply iff_of_false _ h.not_ge
rintro ⟨z, hz⟩
have hz' := hz
rw [← veblen_veblen_of_lt h, hz', veblen_opow_eq_opow_iff] at hz
exact (lt_veblen_invVeblen₁ x).ne' hz
