invVeblen₂_eq_iff — Mathlib

English

For all x, invVeblen₂ x = a if and only if ω^x = veblen (invVeblen₁ x) a.

Русский

Для всех x верно: invVeblen₂ x = a тогда и только тогда, когда ω^x = veblen (invVeblen₁ x) a.

LaTeX

$$$\mathrm{invVeblen}_2 x = a \iff \omega^x = \mathrm{veblen}(\mathrm{invVeblen}_1 x) a$$$

Lean4

theorem invVeblen₂_eq_iff : invVeblen₂ x = a ↔ ω ^ x = veblen (invVeblen₁ x) a := by
  rw [← veblen_inj (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]

Похожие утверждения