principal_opow_omega0

Mathlib.SetTheory.Ordinal.Principal

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

Lean4

theorem principal_opow_omega0 : Principal (· ^ ·) ω := fun a b ha hb =>
  match a, b, lt_omega0.1 ha, lt_omega0.1 hb with
  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by
    simp_rw [← natCast_opow]
    apply nat_lt_omega0

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

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

Разделы

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

Аффилиация

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