Theorems · Theorem · logic and foundations

Ordinal.typein_enum

∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {o : Ordinal.{u}} (h : o < Ordinal.type r),
  (Ordinal.typein r).toRelEmbedding ((Ordinal.enum r) ⟨o, h⟩) = o

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

13 results in Mathlib

Foundations

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

Assumes

IsWellOrder