Theorems · Theorem · logic and foundations

Ordinal.type_lift_preimage

∀ {α : Type u} {β : Type v} (r : α → α → Prop) [inst : IsWellOrder α r] (f : β ≃ α),
  Ordinal.lift.{u, v} (Ordinal.type (⇑f ⁻¹'o r)) = Ordinal.lift.{v, u} (Ordinal.type r)

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

IsWellOrder