-
Notifications
You must be signed in to change notification settings - Fork 298
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(topology/algebra/ordered): conditions for a strictly monotone function to be a homeomorphism #3843
Conversation
This looks good to me. The only thing is I'm not sure about placing lemmas in a file just for the import, but it's up to maintainers to decide about this. |
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 working on this! I left a few comments, otherwise LGTM.
AFAIK, no. And it should be a |
I made the changes from @urkud's review. In the meantime I noticed the existence of I would be very happy to rewrite the relevant parts of this PR to use the bundled versions (maybe it's better to wait until #3838 is merged and use the new terminology). But @urkud (or others), please tell me what you think. |
Thanks! bors r+ |
…nction to be a homeomorphism (#3843) If a strictly monotone function between linear orders is surjective, it is a homeomorphism. If a strictly monotone function between conditionally complete linear orders is continuous, and tends to `+∞` at `+∞` and to `-∞` at `-∞`, then it is a homeomorphism. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Order.20topology) Co-authored by: Yury Kudryashov <urkud@ya.ru> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Pull request successfully merged into master. Build succeeded: |
…nction to be a homeomorphism (#3843) If a strictly monotone function between linear orders is surjective, it is a homeomorphism. If a strictly monotone function between conditionally complete linear orders is continuous, and tends to `+∞` at `+∞` and to `-∞` at `-∞`, then it is a homeomorphism. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Order.20topology) Co-authored by: Yury Kudryashov <urkud@ya.ru> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…nction to be a homeomorphism (#3843) If a strictly monotone function between linear orders is surjective, it is a homeomorphism. If a strictly monotone function between conditionally complete linear orders is continuous, and tends to `+∞` at `+∞` and to `-∞` at `-∞`, then it is a homeomorphism. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Order.20topology) Co-authored by: Yury Kudryashov <urkud@ya.ru> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
If a strictly monotone function between linear orders is surjective, it is a homeomorphism.
If a strictly monotone function between conditionally complete linear orders is continuous, and tends to
+∞
at+∞
and to-∞
at-∞
, then it is a homeomorphism.Zulip discussion
Co-authored by: Yury Kudryashov urkud@ya.ru
Initially, I intended to prove these results in a relative form, using
strict_mono_on
andsurj_on
(for intervals).It turned out much cleaner not to do them in relative form, and hopefully the interval versions can still be deduced from this version (using subtypes). Does mathlib have a
conditionally_complete_linear_order
instance for intervals in aconditionally_complete_linear_order
? I looked but couldn't find one.