principal_mul_omega0_opow_opow

Mathlib.SetTheory.Ordinal.Principal

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

← MathLib Explorer

English

For any ordinal o, Principal (· * ·) (ω^ω^o).

Русский

Для любого ординала o: Principal (· * ·) (ω^ω^o).

LaTeX

$$$Principal(\cdot * \cdot, \omega^{\omega^o}).$$$

Lean4

theorem principal_mul_omega0_opow_opow (o : Ordinal) : Principal (· * ·) (ω ^ ω ^ o) :=
  principal_mul_iff_mul_left_eq.2 fun _ => mul_omega0_opow_opow

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

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

Разделы

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

Аффилиация

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