Trichotomy of well-ordered sets

Stream: Is there code for X?

[Lean tester]

Screenshot 2025-11-03 150522.png
Trying to find a proof for this in mathlib, and figured it may be in ## Mathlib.SetTheory.Ordinal.Basic, but not finding quite this. Is it in there? I'm trying to implement this myself and am finding it quite involved.

[Lean tester]

Oops, wrong place.

[Lean tester]

Screenshot 2025-11-03 150522.png
Trying to find a proof for this in mathlib, and figured it may be in ## Mathlib.SetTheory.Ordinal.Basic, but not finding quite this. Is it in there? I'm trying to implement this myself and am finding it quite involved. Of course, this book does have a theorem later that sorta makes this one redundant.

[Lean tester]

However, couldn't find that other theorem either (every well-ordered set is isomorphic to a unique ordinal).

[Lean tester]

Though, if one looks at the details of the other theorem, it seems to sorta almost make the exact same reasoning as this here, worded differently.

[Aaron Liu]

Lean tester said:

However, couldn't find that other theorem either (every well-ordered set is isomorphic to a unique ordinal).

that's docs#Ordinal.type

[Notification Bot]

2 messages were moved here from #Is there code for X? > left exactness of hom by Ruben Van de Velde.

[Aaron Liu]

there's also docs#InitialSeg.total