IsSuccLimit

Stream: maths

[Yury G. Kudryashov]

@Violeta Hernández Is it intentional that docs#Order.IsSuccLimit allows bot while docs#Ordinal.IsLimit and docs#Cardinal.IsLimit don't?

[Yury G. Kudryashov]

Should we change IsSuccLimit to assume ¬IsMin a (or ¬IsBot a?)

[Yury G. Kudryashov]

CC @Yaël Dillies

[Yaël Dillies]

This was already discussed at length in !3#15005. Upshot is that is_succ_limit is the useful predicate in general, but the literature is divided on whether 0 is a limit ordinal. Eg my Logic & Set Theory lectures this year claim it is, but Wikipedia claims the opposite.

[Yaël Dillies]

Personally I'm in favour of changing cardinal.is_limit to allow 0, or maybe to rename is_succ_limit to is_succ_prelimit and define a new is_succ_limit that matches cardinal.is_limit.

[Kevin Buzzard]

I wouldn't trust "random lecturer who doesn't really care about the question" any more.

[Kevin Buzzard]

However I think I agree with your random lecturer!

[Violeta Hernández]

I've got nothing new to say here but I might as well say hi

[Violeta Hernández]

Long time no see

[Yury G. Kudryashov]

From topology point of view, {0} is an open set while all other {c}, IsSuccLimit c are.

[Yury G. Kudryashov]

I will think about the IsSuccPrelimit option.

[Pedro Sánchez Terraf]

I'm definitely with the topology camp on this one, and since 0 is isolated, it is not a limit. Nor obviously a successor.

[Kevin Buzzard]

From the order point of view, 0 is the sup of the ordinals strictly less than it, so it's a limit ordinal. But maybe it's like 1 not being a prime despite it satisfying many of the criteria for and properties of primality.

[Pedro Sánchez Terraf]

You just have proved that a sup need not be a limit :wink:

[Pedro Sánchez Terraf]

Yury G. Kudryashov said:

Violeta Hernández Is it intentional that docs#Order.IsSuccLimit allows bot while docs#Ordinal.IsLimit and docs#Cardinal.IsLimit don't?

Wrt cardinals, limit is only used for infinite ones.