card_le_of_le_ord — Mathlib

English

For every ordinal o and cardinal c, if o ≤ c.ord, then o.card ≤ c.

Русский

Для любого ординала o и кардинала c если o ≤ c.ord, то o.card ≤ c.

LaTeX

$$$ o \le c.\operatorname{ord} \implies |o| \le c $$$

Lean4

/-- A variation on `Cardinal.lt_ord` using `≤`: If `o` is no greater than the
initial ordinal of cardinality `c`, then its cardinal is no greater than `c`.

The converse, however, is false (for instance, `o = ω+1` and `c = ℵ₀`).
-/
theorem card_le_of_le_ord {o : Ordinal} {c : Cardinal} (ho : o ≤ c.ord) : o.card ≤ c := by rw [← card_ord c];
  exact Ordinal.card_le_card ho

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