no injective function on `ordinal`

Stream: Is there code for X?

[Sebastien Gouezel]

Is there already a lemma saying that ordinal.{u} is bigger than any type in Type u?

lemma foo {β : Type u} (f : ordinal.{u} → β) : ¬ (function.injective f) :=

[Reid Barton]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Transfinite.20recursion/near/253614140