invVeblen₁_veblen — Mathlib

English

If a < veblen o a, then invVeblen₁ (veblen o a) = o.

Русский

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

LaTeX

$$$\text{If } a < \mathrm{veblen}(o, a),\ \mathrm{invVeblen}_1(\mathrm{veblen}(o, a)) = o.$$$

Lean4

theorem invVeblen₁_veblen (h : a < veblen o a) : invVeblen₁ (veblen o a) = o :=
  by
  apply le_antisymm
  · rwa [← lt_veblen_iff_invVeblen₁_le, veblen_lt_veblen_iff_right]
  · rw [← mem_range_veblen_iff_le_invVeblen₁]
    obtain rfl | ho := eq_zero_or_pos o
    · simp
    · rw [← veblen_zero_apply, veblen_veblen_of_lt ho]
      simp

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