[Merged by Bors] - feat(data/set/basic,order/filter/basic): add semiconj lemmas about images and maps #14970
Conversation
…with more useful API `_comm` lemmas are usually of the form `f (g x) = g (f x)`, but this lemma was of the form `f1 (f2 x) = f3 (f4 x)` which isn't commutativity in the usual sense. This adds a `function.commute` and `function.semiconj` lemma, and renames `image_comm` to `image_image_eq_image_image_of_eq`..
eric-wieser
added
awaiting-review
There was a problem hiding this comment.
I am happy with the semiconj and commute lemmas (although I would like to see finset and filter versions as well), but image_image_eq_image_image_of_eq is a terrible name that goes against the naming conventions around algebraic replacement rules: see set.image2_comm, set.image2_assoc, the second half of data.finset.n_ary, the second half of data.filter.n_ary.
|
The finset lemmas can't exist until #14963 goes in, I'm working on the |
eric-wieser
changed the title
set.image_comm with more useful API
|
It's a matter of "commutativity in a group" vs "commutativity in a groupoid". Do you have examples of groupoids that are also groups in an incompatible way? If not, I think the naming convention can stay as such because the two use cases are analogous and disjoint. |
Both are now added |
github-actions
bot
removed
the
awaiting-CI
|
Thanks! |
github-actions
bot
added
ready-to-merge
…ages and maps (#14970) This adds `function.commute` and `function.semiconj` lemmas, and replaces all the uses of `_comm` lemmas with the `semiconj` version as it turns out that only this generality is needed.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This adds
function.commuteandfunction.semiconjlemmas, and replaces all the uses of_commlemmas with thesemiconjversion as it turns out that only this generality is needed.