Theorems · Theorem · logic and foundations

OrderIso.ordinalType_congr

∀ {α β : Type u_1} [inst : LinearOrder α] [inst_1 : LinearOrder β] [inst_2 : WellFoundedLT α] [inst_3 : WellFoundedLT β]
  (h : α ≃o β), (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.type fun x1 x2 => x1 < x2

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderLinearOrderWellFoundedLTWellFoundedLT