-
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(order/filter/basic): add map_le_map
and map_injective
#15128
Conversation
src/order/filter/basic.lean
Outdated
lemma map_le_map {f g : filter α} {m : α → β} (hm : injective m) : map m f ≤ map m g ↔ f ≤ g := | ||
by rw [map_le_iff_le_comap, comap_map hm] |
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.
Isn't this just a weaker version of the bizarrely-named le_of_map_le_map_inj_iff
above?
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.
(which should probably be named map_le_map_iff_of_inj_on
and be stated using set.inj_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.
Renamed, removed ->
versions in favor of iff
s.
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.
@eric-wieser Could you please have another look?
bors merge Thanks! |
* Add `filter.map_le_map`, an `iff` version of `filter.map_mono`. * Add `filter.map_injective`, a `function.injective` version of `filter.map_inj`.
Pull request successfully merged into master. Build succeeded: |
map_le_map
and map_injective
map_le_map
and map_injective
filter.map_le_map
, aniff
version offilter.map_mono
.filter.map_injective
, afunction.injective
version offilter.map_inj
.