-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(order): countable categoricity of dense linear orders #2860
Conversation
@dwarn is this still WIP? |
@robertylewis Sorry, I haven't done any Lean these past few months and sort of abandoned this PR. I had a look just now to bring it up to date with current mathlib and also add a stub about order embeddings. This will prove for example that any countable ordinal embeds in the reals. There's still a bit of work required to make this mergeable (move some lemmas as Bhavik suggested, finish construction of order embedding, naming, doc strings, ...). |
@dwarn Okay, great! In that case we'll leave the PR open and tagged as it is. Whenever you're ready, please change the label to "awaiting review." |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sorry, a few more style nitpicks.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you for picking up this PR again! I have a few remarks, but overall it looks great.
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Thank you 🎉 bors r+ |
Thanks to all reviewers! |
We construct an order isomorphism between any two countable, nonempty, dense linear orders without endpoints, using the back-and-forth method.
Pull request successfully merged into master. Build succeeded: |
We construct an order isomorphism between any two countable, nonempty, dense linear orders without endpoints, using the back-and-forth method.
Blocked by #2850