[Merged by Bors] - feat: Eventual boundedness of neighborhoods #8009
Conversation
YaelDillies
added
awaiting-review
| refine ⟨fun x ↦ ?_⟩ | ||
| obtain ⟨a, ha⟩ := isBounded_ge_nhds x.1 | ||
| obtain ⟨b, hb⟩ := isBounded_ge_nhds x.2 | ||
| rw [← @Prod.mk.eta _ _ x, nhds_prod_eq] | ||
| exact ⟨(a, b), ha.prod_mk hb⟩ |
There was a problem hiding this comment.
instead of copying the proof, you can deduce it from the other one by order-dual arguments, with something like
| refine ⟨fun x ↦ ?_⟩ | |
| obtain ⟨a, ha⟩ := isBounded_ge_nhds x.1 | |
| obtain ⟨b, hb⟩ := isBounded_ge_nhds x.2 | |
| rw [← @Prod.mk.eta _ _ x, nhds_prod_eq] | |
| exact ⟨(a, b), ha.prod_mk hb⟩ | |
| ⟨(instBoundedLENhdsClassProd (α := αᵒᵈ) (β := βᵒᵈ)).isBounded_le_nhds⟩ |
(if you have named the instance above). Same thing for the next instance.
There was a problem hiding this comment.
Since this is a forward-port PR, I think this is best left to a follow-up. The ideal place for this comment would have been leanprover-community/mathlib#18629!
sgouezel
added
awaiting-author
|
This looks like a faithful forward-port, so bors merge Please open a follow-up PR to address @sgouezel's concerns. |
|
Canceled. |
github-actions
bot
removed
the
awaiting-author
|
bors merge |
Forward port leanprover-community/mathlib#18629 Co-authored-by: Eric Wieser <wieser.eric@gmail.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. |
bors
bot
changed the title
Forward port leanprover-community/mathlib#18629