principal_opow — Mathlib

English

For any cardinal c, the opow operation on ordinals yields a principal structure over c.ord.

Русский

Для любого кардинала c операция возведения в степень над ординалами порождает простую структуру над c.ord.

LaTeX

$$Principal (·^·) c.ord$$

Lean4

theorem principal_opow {o : Ordinal} (h : IsInitial o) (ho : ω ≤ o) : Principal (· ^ ·) o :=
  by
  obtain ⟨a, rfl⟩ := mem_range_omega_iff.2 ⟨ho, h⟩
  exact principal_opow_omega a

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