gamma0_le_of_veblen_le

Mathlib.SetTheory.Ordinal.Veblen

URI: https://scilib.ai/kg/mathlib#Ordinal.gamma0_le_of_veblen_le

← MathLib Explorer

English

If veBlen o 0 ≤ o, then Γ₀ ≤ o.

Русский

Если veblen o 0 ≤ o, то Γ₀ ≤ o.

LaTeX

$$$(\\veblen o 0) \\le o \\Rightarrow Γ_0 \\le o$$$

Lean4

theorem gamma0_le_of_veblen_le (h : veblen o 0 ≤ o) : Γ₀ ≤ o :=
  by
  rw [gamma0_eq_nfp]
  exact nfp_le_fp (veblen_left_monotone 0) (Ordinal.zero_le o) h

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

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

Разделы

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

Аффилиация

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