-
Notifications
You must be signed in to change notification settings - Fork 259
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: general Ascoli theorem #6844
Conversation
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.
This is awesome! My only regret is that I could not come up with any non-trivial suggestions while reviewing.
bors d+
|
||
* In Bourbaki, the usual Arzela-Ascoli compactness theorem follows from a similar total boundedness | ||
result. Here we go directly for the compactness result, which is the most useful in practice, but | ||
this will be an easy addition/refactor if we ever need it. |
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.
Could you clarify what you mean by "this" here: I presume you mean establishing the intermediate total boundedness result a la Bourbaki?
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.
Don't you want me to change this before merging? I was planning to do it tomorrow morning. I can also change the wording later if you want.
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.
I decided I was splitting hairs and it wasn't worth delaying this PR any further.
Feel free to follow up with a doc string adjustment PR or not, according to your taste!
✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Oliver Nash <github@olivernash.org>
…hlib4 into AD_ascoli_part1
bors merge |
Co-authored-by: @vbeffara (port to Lean4), @tb65536 (suggested to skip the totally bounded case and go straight to compactness using Tykhonov) This was discussed on Zulip [recently](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Arzela-Ascoli.20for.20uniform.20spaces) and [a while ago](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Montel's.20theorem).
Pull request successfully merged into master. Build succeeded: |
Co-authored-by: @vbeffara (port to Lean4), @tb65536 (suggested to skip the totally bounded case and go straight to compactness using Tykhonov) This was discussed on Zulip [recently](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Arzela-Ascoli.20for.20uniform.20spaces) and [a while ago](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Montel's.20theorem).
Co-authored-by: @vbeffara (port to Lean4), @tb65536 (suggested to skip the totally bounded case and go straight to compactness using Tykhonov) This was discussed on Zulip [recently](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Arzela-Ascoli.20for.20uniform.20spaces) and [a while ago](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Montel's.20theorem).
Co-authored-by: @vbeffara (port to Lean4), @tb65536 (suggested to skip the totally bounded case and go straight to compactness using Tykhonov) This was discussed on Zulip [recently](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Arzela-Ascoli.20for.20uniform.20spaces) and [a while ago](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Montel's.20theorem).
Co-authored-by: @vbeffara (port to Lean4), @tb65536 (suggested to skip the totally bounded case and go straight to compactness using Tykhonov) This was discussed on Zulip [recently](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Arzela-Ascoli.20for.20uniform.20spaces) and [a while ago](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Montel's.20theorem).
Co-authored-by: @vbeffara (port to Lean4), @tb65536 (suggested to skip the totally bounded case and go straight to compactness using Tykhonov)
This was discussed on Zulip recently and a while ago.