lt_veblen_iff_invVeblen₁_le — Mathlib

English

For any ordinals a and o, a < veblen o a if and only if invVeblen₁ a ≤ o.

Русский

Для любых ординалов a и o верно: a < veblen(o, a) тогда и только тогда, когда invVeblen₁ a ≤ o.

LaTeX

$$$a < \mathrm{veblen}(o, a) \iff \mathrm{invVeblen}_1 a \le o$$$

Lean4

theorem lt_veblen_iff_invVeblen₁_le : a < veblen o a ↔ invVeblen₁ a ≤ o :=
  by
  obtain h | h := lt_or_ge o (invVeblen₁ a)
  · rw [veblen_eq_of_lt_invVeblen₁ h]
    simpa
  · simpa [(lt_veblen_invVeblen₁ a).trans_le (veblen_left_monotone _ h)]

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