lt_veblen_invVeblen₁ — Mathlib

English

Let x be an ordinal. Then x is strictly less than the Veblen function applied to invVeblen₁ x and x; that is, x < veblen (invVeblen₁ x) x.

Русский

Пусть x — ординал. Тогда x строго меньше функции Веблена, применённой к invVeblen₁ x и x; то есть x < veblen (invVeblen₁ x) x.

LaTeX

$$$x < \mathrm{veblen}(\mathrm{invVeblen}_1 x, x)$$$

Lean4

theorem lt_veblen_invVeblen₁ (x : Ordinal) : x < veblen (invVeblen₁ x) x :=
  (right_le_veblen ..).lt_of_ne' (csInf_mem (s := {y | veblen y x ≠ x}) ⟨x, (lt_veblen x).ne'⟩)

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