invVeblen₂_veblen — Mathlib

English

If o ≠ 0 and a < veblen o a, then invVeblen₂ (veblen o a) = a.

Русский

Если o ≠ 0 и a < veblen o a, то invVeblen₂ (veblen o a) = a.

LaTeX

$$$o \neq 0 \land a < \mathrm{veblen}(o,a) \Rightarrow invVeblen_2(\mathrm{veblen}(o,a)) = a$$$

Lean4

theorem invVeblen₂_veblen (ho : o ≠ 0) (h : a < veblen o a) : invVeblen₂ (veblen o a) = a :=
  by
  rw [invVeblen₂_eq_iff, invVeblen₁_veblen h, ← veblen_zero_apply, veblen_veblen_of_lt]
  exact ho.bot_lt

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