-
Notifications
You must be signed in to change notification settings - Fork 299
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(analysis/normed_space/dual): add lemmas, golf #11132
Conversation
* add `polar_univ`, `is_closed_polar`, `polar_gc`, `polar_Union`, `polar_union`, `polar_antitone`, `polar_zero`, `polar_closure`; * extract `polar_ball_subset_closed_ball_div` and `closed_ball_inv_subset_polar_closed_ball` out of the proofs of `polar_closed_ball` and `polar_bounded_of_nhds_zero`; * rename `polar_bounded_of_nhds_zero` to `bounded_polar_of_mem_nhds_zero`, use `metric.bounded`; * use `r⁻¹` instead of `1 / r` in `polar_closed_ball`. This is the simp normal form (though we might want to change this in the future).
This PR/issue depends on:
|
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.
bors d+
variable (E) | ||
|
||
lemma polar_gc : | ||
galois_connection (order_dual.to_dual ∘ polar 𝕜) |
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 think this order_dual.to_dual ∘
is worth a docstring comment.
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
bors merge |
* add `polar_univ`, `is_closed_polar`, `polar_gc`, `polar_Union`, `polar_union`, `polar_antitone`, `polar_zero`, `polar_closure`; * extract `polar_ball_subset_closed_ball_div` and `closed_ball_inv_subset_polar_closed_ball` out of the proofs of `polar_closed_ball` and `polar_bounded_of_nhds_zero`; * rename `polar_bounded_of_nhds_zero` to `bounded_polar_of_mem_nhds_zero`, use `metric.bounded`; * use `r⁻¹` instead of `1 / r` in `polar_closed_ball`. This is the simp normal form (though we might want to change this in the future).
Pull request successfully merged into master. Build succeeded: |
* add `polar_univ`, `is_closed_polar`, `polar_gc`, `polar_Union`, `polar_union`, `polar_antitone`, `polar_zero`, `polar_closure`; * extract `polar_ball_subset_closed_ball_div` and `closed_ball_inv_subset_polar_closed_ball` out of the proofs of `polar_closed_ball` and `polar_bounded_of_nhds_zero`; * rename `polar_bounded_of_nhds_zero` to `bounded_polar_of_mem_nhds_zero`, use `metric.bounded`; * use `r⁻¹` instead of `1 / r` in `polar_closed_ball`. This is the simp normal form (though we might want to change this in the future).
add
polar_univ
,is_closed_polar
,polar_gc
,polar_Union
,polar_union
,polar_antitone
,polar_zero
,polar_closure
;extract
polar_ball_subset_closed_ball_div
andclosed_ball_inv_subset_polar_closed_ball
out of the proofs ofpolar_closed_ball
andpolar_bounded_of_nhds_zero
;rename
polar_bounded_of_nhds_zero
tobounded_polar_of_mem_nhds_zero
, usemetric.bounded
;use
r⁻¹
instead of1 / r
inpolar_closed_ball
. This is thesimp normal form (though we might want to change this in the future).
a / a ≤ 1
#11118