Theorems · Theorem · logic and foundations

Cardinal.card_typein_lt

∀ {α : Type u} {r : α → α → Prop} [inst : IsWellOrder α r] (x : α),
  (Cardinal.mk α).ord = Ordinal.type r → ((Ordinal.typein r).toRelEmbedding x).card < Cardinal.mk α

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

IsWellOrder