Long line

Stream: Is there code for X?

[Yaël Dillies]

Do we have anything about the long line? If not, I think formalizing some counterexamples coming from it is a good first project.

[Patrick Massot]

I think that focusing on easy targets from the undergrad list is a much better first project that adding some more exotic stuff to mathlib.

[Stuart Presnell]

On the other hand, looking at counterexamples is a good way to see why certain things are defined just as they are.