RFC: ditch Ordinal.IsLimit

Stream: mathlib4

[Violeta Hernández]

Here's my hot take of the day: we don't need docs#Ordinal.IsLimit

[Violeta Hernández]

We already have docs#Order.IsSuccLimit. The only difference between the two is that IsSuccLimit 0 but ¬ IsLimit 0. I really don't think this warrants the need for a separate definition with separate API.

[Violeta Hernández]

I don't think the definition is useless. Important results like docs#Ordinal.IsNormal.isLimit do require we omit the o = 0 case. But I think the inconvenience of having to specify IsSuccLimit o and o ≠ 0 separately is outweighed by the inconvenience of having nearly duplicate APIs for IsLimit and IsSuccLimit.

[Violeta Hernández]

Likewise, I don't think we should ditch docs#Ordinal.limitRecOn, just that we should specify o ≠ 0 as a hypothesis in the limit case. We already have docs#SuccOrder.limitRecOn for the cases where that's applicable.

[Yury G. Kudryashov]

See also #maths > IsSuccLimit

[Violeta Hernández]

Oh! I had forgotten about that