[Merged by Bors] - feat(Topology/Order/LowerUpperTopology): Dual the lower topology#5873
[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>
ADedecker
left a comment
There was a problem hiding this comment.
One last comment, then this should be good to go!
| constructor | ||
| · apply UpperTopology.instLowerTopologyOrderDualInstTopologicalSpaceOrderDualPreorder | ||
| · apply LowerTopology.instUpperTopologyOrderDualInstTopologicalSpaceOrderDualPreorder |
There was a problem hiding this comment.
| constructor | |
| · apply UpperTopology.instLowerTopologyOrderDualInstTopologicalSpaceOrderDualPreorder | |
| · apply LowerTopology.instUpperTopologyOrderDualInstTopologicalSpaceOrderDualPreorder | |
| constructor <;> intro _ <;> infer_instance |
If that works. Same below
There was a problem hiding this comment.
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.
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?
|
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?