invVeblen₂_le

Mathlib.SetTheory.Ordinal.Veblen

URI: https://scilib.ai/kg/mathlib#Ordinal.invVeblen₂_le

← MathLib Explorer

English

invVeblen₂ x ≤ x for all x.

Русский

invVeblen₂ x ≤ x для любого x.

LaTeX

$$$invVeblen_2 x \le x$$$

Lean4

theorem invVeblen₂_le (x : Ordinal) : invVeblen₂ x ≤ x :=
  by
  obtain h | h := eq_zero_or_pos (invVeblen₁ x)
  · rw [invVeblen₂_le_iff, h, veblen_zero]
  · convert (invVeblen₂_lt x).le
    rw [← veblen_zero_apply, veblen_eq_of_lt_invVeblen₁ h]

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

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

Разделы

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

Аффилиация

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