Theorems · Theorem · logic and foundations

WellOrder.mk.inj

∀ {α : Type u} {r : α → α → Prop} {wo : IsWellOrder α r} {α_1 : Type u} {r_1 : α_1 → α_1 → Prop}
  {wo_1 : IsWellOrder α_1 r_1}, { α := α, r := r, wo := wo } = { α := α_1, r := r_1, wo := wo_1 } → α = α_1 ∧ r ≍ r_1

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

1 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms