ordinal.infinite

Stream: maths

[Johan Commelin]

@Violeta Hernández @Eric Rodriguez What do you think of introducing

def ordinal.infinite (o : ordinal) : Prop := \omega \le o

It seems to be a common condition, and it would enable dot-notation.

[Kevin Buzzard]

I see that Chris' formalisation of "alg closed fields of the same uncountable cardinality and characteristic are isomorphic" used "cardinal.omega < #K so maybe cardinal.uncountable` and other similar things could also be added?

[Eric Rodriguez]

I feel like the le dot notation works fairly well in this case, but in any case I'm not a big user of the cardinal stuff, so I don't think I should make the decision

[Mario Carneiro]

The motivation here seems kind of weak

[Mario Carneiro]

I think \omega <= c or \omega < c is plenty readable as is

[Violeta Hernández]

I put my thoughts on GitHub already, that this would obscure a very simple definition

[Violeta Hernández]

Surely in most cases it's much easier to treat this as an inequality