Theorems · Definition · logic and foundations

Ordinal.lift

Ordinal.{v} → Ordinal.{max v u}

The universe lift operation for ordinals, which embeds Ordinal.{u} as a proper initial segment of Ordinal.{v} for v > u. For the initial segment version, see liftInitialSeg.

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

86 results in Mathlib

Foundations

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