principal_mul — Mathlib

English

Let o be an ordinal that is initial and ω ≤ o. Then o is multiplicatively principal: for all a,b < o, a · b < o.

Русский

Пусть o — ординал, являющийся начальным и удовлетворяющий ω ≤ o. Тогда o является мультипликативно принципиальным: для всех a,b < o выполняется a · b < o.

LaTeX

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

Lean4

theorem principal_mul {o : Ordinal} (h : IsInitial o) (ho : ω ≤ o) : Principal (· * ·) o :=
  by
  rw [← h.ord_card]
  apply principal_mul_ord
  rwa [aleph0_le_card]

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