veblen_invVeblen₁_invVeblen₂

Mathlib.SetTheory.Ordinal.Veblen

URI: https://scilib.ai/kg/mathlib#Ordinal.veblen_invVeblen₁_invVeblen₂

← MathLib Explorer

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

$$$\text{If } o \neq 0 \text{ and } a < \mathrm{veblen}(o,a),\ \mathrm{invVeblen}_2(\mathrm{veblen}(o,a)) = a$$$

Lean4

@[simp]
theorem veblen_invVeblen₁_invVeblen₂ (x : Ordinal) : veblen (invVeblen₁ x) (invVeblen₂ x) = ω ^ x :=
  Classical.choose_spec (mem_range_veblen_iff_le_invVeblen₁.2 le_rfl)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru