principal_add_omega — Mathlib

English

For every ordinal o, the ordinal ω_o is a principal element with respect to addition.

Русский

Для любого ординала o, ординал ω_o является принципиальным элементом относительно операции сложения.

LaTeX

$$$\forall o,\ \operatorname{Principal}(+,\omega_o)$$$

Lean4

theorem principal_add_omega (o : Ordinal) : Principal (· + ·) (ω_ o) :=
  (isInitial_omega o).principal_add (omega0_le_omega o)

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