isNormal_opow — Mathlib

English

If a > 1, then the function x ↦ a^x is a normal function on ordinals.

Русский

Если a > 1, то функция x ↦ a^x есть нормальная функция на ординалах.

LaTeX

$$$1 < a \Rightarrow \mathrm{IsNormal}(x \mapsto a^x)\,\text{ on ordinals}$$$

Lean4

theorem isNormal_opow {a : Ordinal} (h : 1 < a) : IsNormal (a ^ ·) :=
  by
  have ha : 0 < a := zero_lt_one.trans h
  refine IsNormal.of_succ_lt ?_ fun hl ↦ ?_
  · simpa only [mul_one, opow_succ] using fun b ↦ mul_lt_mul_of_pos_left h (opow_pos b ha)
  · simp [IsLUB, IsLeast, upperBounds, lowerBounds, ← opow_le_of_isSuccLimit ha.ne' hl]

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