Theorems · Theorem · logic and foundations

Cardinal.card_le_of_le_ord

∀ {o : Ordinal.{u_1}} {c : Cardinal.{u_1}}, o ≤ c.ord → o.card ≤ c

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 = ℵ₀).

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

1 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound