Scattered orders

Stream: mathlib4

[Erica Assang]

Hi all! I’m Erica, an undergrad at CMU, and I recently formalized Hausdorff’s characterization of scattered orders with the help of Profs. Jeremy Avigad and James Cummings. Is this something that would be a good fit for mathlib?

More precisely, the main theorem is: the set of scattered orders (those which do not contain a copy of the rationals) is equal to the smallest set of linear orders containing every singleton order and that is closed under well-ordered and reverse well-ordered lexicographic sums. The project also contains a proof that every linear order has a well-ordered cofinal subset.

Here is the repo: https://github.com/avoair/Hausdorff.git

[Yaël Dillies]

That looks like something @Bhavik Mehta would be very interested in!

[Bhavik Mehta]

Yes, these orders also came up for me a few times! I think this definition would make sense for mathlib

[Bhavik Mehta]

The stuff in #28278 looks like it'll be relevant for you too, eg your definition of Scattered is equivalent to $\eta \nleq \alpha$ (where $\eta$ is the order type of the rationals)

[Yaël Dillies]

cc @Yan Yablonovskiy 🇺🇦

[Eric Paul]

Awesome, I'm excited to see this formalized!

I'm also quite interested in lots of relations like your hausdorffScattered_rel, i.e. equivalence relations where the equivalence classes are intervals in the linear order. I think it'd be great to have these convex equivalence relations and their theory for linear orders in mathlib.

[Yan Yablonovskiy 🇺🇦]

I have order types with some basics and the order type of rationals/ order on order types , in fact it may already be enough to define what you like: OrderTypes . It’s a bit old though, I am about to merge more recent code and try get some into Mathlib potentially.

[Erica Assang]

Thank you all for the references and feedback! @Yan Yablonovskiy 🇺🇦 that looks great. I think reframing some of my definitions in terms of order types could definitely tighten things up -- I will see what I can do!