principal_mul_ord — Mathlib

English

Let c be a cardinal with ω ≤ c. Then the ordinal c.ord is closed under ordinal multiplication: for all a,b < c.ord, a · b < c.ord.

Русский

Пусть c — кардинал с ω ≤ c. Тогда ординал c.ord замкнут относительно ординального умножения: для любых a,b < c.ord верно a · b < c.ord.

LaTeX

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

Lean4

theorem principal_mul_ord {c : Cardinal} (hc : ℵ₀ ≤ c) : Principal (· * ·) c.ord :=
  by
  intro a b ha hb
  rw [lt_ord, card_mul] at *
  exact mul_lt_of_lt hc ha hb

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