isSuccLimit_opow

Mathlib.SetTheory.Ordinal.Exponential

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

English

If a > 1, then IsSuccLimit b implies IsSuccLimit (a^b).

Русский

Если a > 1, то из IsSuccLimit b следует IsSuccLimit (a^b).

LaTeX

$$$1 < a \Rightarrow IsSuccLimit(b) \Rightarrow IsSuccLimit(a^b)$$$

Lean4

theorem isSuccLimit_opow {a b : Ordinal} (a1 : 1 < a) : IsSuccLimit b → IsSuccLimit (a ^ b) :=
  (isNormal_opow a1).isSuccLimit

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

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

Разделы

Аффилиация

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