principal_mul_omega — Mathlib

English

For any ordinal o, the ordinal ω_o is multiplicatively principal: if a,b < ω_o then a · b < ω_o.

Русский

Для произвольного ординала o ординал ω_o является мультипликативно принципиальным: если a,b < ω_o, то a · b < ω_o.

LaTeX

$$$\forall a,b\,(a < \omega_o \rightarrow b < \omega_o \rightarrow a \cdot b < \omega_o).$$$

Lean4

theorem principal_mul_omega (o : Ordinal) : Principal (· * ·) (ω_ o) :=
  (isInitial_omega o).principal_mul (omega0_le_omega o)

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