opow_lt_veblen_opow_iff

Mathlib.SetTheory.Ordinal.Veblen

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

English

For all a, ω^a < veblen(o, ω^a) iff a < veblen(o,a).

Русский

Для всех a верно ω^a < veblen(o, ω^a) тогда и только тогда a < veblen(o,a).

LaTeX

$$$$\\omega^{a} < \\operatorname{veblen}(o, \\omega^{a}) \\iff a < \\operatorname{veblen}(o,a).$$$$

Lean4

theorem opow_lt_veblen_opow_iff : ω ^ a < veblen o (ω ^ a) ↔ a < veblen o a :=
  apply_lt_veblenWith_apply_iff (isNormal_opow one_lt_omega0)

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

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

Разделы

Аффилиация

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