-
Notifications
You must be signed in to change notification settings - Fork 235
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/Order/LowerUpperTopology): Dual the lower topology #5873
Conversation
I couldn't see how to deduce
from
I think I need some way of identifying |
Sorry for not commenting earlier, I'll review tomorrow. |
Thanks very much - I appreciate I must have taken up a lot of people's time with my PRs. |
You shouldn't have to worry about that, your contributions are definitely welcome and your code is looking good, so time spent reviewing it is time well-spent! |
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Co-authored-by: Anatole Dedecker <anatolededecker@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.
One last comment, then this should be good to go!
constructor | ||
· apply UpperTopology.instLowerTopologyOrderDualInstTopologicalSpaceOrderDualPreorder | ||
· apply LowerTopology.instUpperTopologyOrderDualInstTopologicalSpaceOrderDualPreorder |
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.
constructor | |
· apply UpperTopology.instLowerTopologyOrderDualInstTopologicalSpaceOrderDualPreorder | |
· apply LowerTopology.instUpperTopologyOrderDualInstTopologicalSpaceOrderDualPreorder | |
constructor <;> intro _ <;> infer_instance |
If that works. Same below
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.
Unfortunately
lemma UpperDual_iff_Lower [Preorder α] [TopologicalSpace α] :
UpperTopology αᵒᵈ ↔ LowerTopology α := by
constructor <;> intro _ <;> infer_instance
gives me
failed to synthesize instance
LowerTopology α
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.
Ah right because it doesn't know how to go backwards. Then let's keep the current proof. Could you just give an explicit name to the instances so that it looks better?
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.
Done, thanks.
Thanks! maintainer merge |
🚀 Pull request has been placed on the maintainer queue by ADedecker. |
bors merge |
Defines the upper topology, which is the dual of the lower topology on a preorder. Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com> Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Defines the upper topology, which is the dual of the lower topology on a preorder. Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com> Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Defines the upper topology, which is the dual of the lower topology on a preorder.
As requested by @YaelDillies and @ADedecker .
I have put the lower and upper topologies in the same file. However, this may complicate the lean4 porting effort, so it may be better to keep the files separate whilst mathlib and mathlib4 are being kept in sync?