Ordinal division algorithm
ID: ordinal-division-algorithm
For ordinals and , there are unique ordinals with the displayed relation. The function is strictly increasing, continuous at limit ordinals and unbounded. Its first value above occurs at a successor, giving the largest with . The ordered tail of after that initial segment gives , and maximality gives .
New to topics? Read the docs here!