veblen_pos

Mathlib.SetTheory.Ordinal.Veblen

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

English

For all o and a, 0 < veblen(o,a).

Русский

Для всех o и a верно 0 < veblen(o,a).

LaTeX

$$$$0 < \\operatorname{veblen}(o,a).$$$$

Lean4

@[simp]
theorem veblen_pos : 0 < veblen o a :=
  veblenWith_pos (isNormal_opow one_lt_omega0) (by simp)

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

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

Разделы

Аффилиация

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