Theorems · Definition · logic and foundations

Ordinal.log

Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}

The ordinal logarithm is the solution u to the equation x = b ^ u * v + w where v < b and w < b ^ u. We special case log 0 x = log 1 x = 0, as well as log b 0 = 0.

Defined in

Mathlib.SetTheory.Ordinal.Exponential

Cited by

45 results in Mathlib

Foundations

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