principal_add_omega0_opow

Mathlib.SetTheory.Ordinal.Principal

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

English

For every ordinal o, Principal (· + ·) (ω^o).

Русский

Для каждого ординала o имеет место Principle (+) (ω^o).

LaTeX

$$$Principal(\cdot + \cdot, \omega^o).$$$

Lean4

theorem principal_add_omega0_opow (o : Ordinal) : Principal (· + ·) (ω ^ o) :=
  principal_add_iff_add_left_eq_self.2 fun _ => add_omega0_opow

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

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

Разделы

Аффилиация

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