veblen_veblen_of_lt

Mathlib.SetTheory.Ordinal.Veblen

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

← MathLib Explorer

English

If o1 < o2, then veblen o1 (veblen o2 a) = veblen o2 a.

Русский

Если o1 < o2, то veblen o1 (veblen o2 a) = veblen o2 a.

LaTeX

$$$\forall o1,o2,a:\operatorname{Ordinal},\ o1 < o2 \Rightarrow \operatorname{veblen}(o1,\operatorname{veblen}(o2,a)) = \operatorname{veblen}(o2,a)$$$

Lean4

theorem veblen_veblen_of_lt (h : o₁ < o₂) (a : Ordinal) : veblen o₁ (veblen o₂ a) = veblen o₂ a :=
  veblenWith_veblenWith_of_lt (isNormal_opow one_lt_omega0) h a

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

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

Разделы

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

Аффилиация

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