principal_opow_omega — Mathlib

English

For every ordinal o, the opow operation forms a principal embedding with base ω0 indexed by o.

Русский

Для каждого ординала o операция возведения в степень образует простой вложение на основе ω0, индексированное o.

LaTeX

$$Principal (·^·) (ω_ o)$$

Lean4

theorem principal_opow_omega (o : Ordinal) : Principal (· ^ ·) (ω_ o) :=
  by
  obtain rfl | ho := Ordinal.eq_zero_or_pos o
  · rw [omega_zero]
    exact principal_opow_omega0
  · intro a b ha hb
    rw [lt_omega_iff_card_lt] at ha hb ⊢
    apply (card_opow_le a b).trans_lt (max_lt _ (max_lt ha hb))
    rwa [← aleph_zero, aleph_lt_aleph]

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