Theorems · Theorem · logic and foundations

Ordinal.not_lt_enum_ord_mk_min_compl

∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {s : Set α} (hfin : s.Finite) (h : sᶜ.Nonempty),
  ¬r ((Ordinal.enum r) ⟨(Cardinal.mk ↑s).ord, ⋯⟩) (⋯.min sᶜ h)

The #s-th element of α is an upper-bound for the set's mex (minimum excluded value), ordered by r, when s is finite. See card_typein_min_le_mk for the Ordinal version.

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

IsWellOrder