Theorems · Theorem · logic and foundations

Ordinal.card_typein_min_le_mk

∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {s : Set α} (hs : sᶜ.Nonempty),
  ((Ordinal.typein r).toRelEmbedding (⋯.min sᶜ hs)).card ≤ Cardinal.mk ↑s

The cardinality of a set is an upper-bound for the cardinality of the order type of the set's mex (minimum excluded value). See not_lt_enum_ord_mk_min_compl for the α version.

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

IsWellOrder