[Merged by Bors] - feat(data/equiv/basic): lemmas about images and preimages #6398
Conversation
gebner
commented
Feb 24, 2021
gebner
commented
gebner
added
the
awaiting-review
| @@ -353,6 +353,29 @@ protected lemma image_compl {α β} (f : equiv α β) (s : set α) : | |||
| f '' sᶜ = (f '' s)ᶜ := | |||
| set.image_compl_eq f.bijective | |||
|
|
|||
| @[simp] lemma symm_preimage_preimage {α β} (e : α ≃ β) (s : set β) : | |||
| e.symm ⁻¹' (e ⁻¹' s) = s := | |||
There was a problem hiding this comment.
Do we have a lemma that says f ⁻¹' (g ⁻¹' s) = (f \comp g) ⁻¹' s or whatever variant of that is true?
There was a problem hiding this comment.
Yes it's called preimage_preimage (as you would expect). That is, a few characters longer than the current proof.
There was a problem hiding this comment.
Right, I ask only because simp would solve this automatically if preimage_preimage were marked simp
There was a problem hiding this comment.
In general I'm not too happy to mark conditional simp lemmas as simp.
There was a problem hiding this comment.
In what way is preimage_preimage conditional?
There was a problem hiding this comment.
Ah sorry, I was looking at the wrong lemma. No, preimage_preimage is indeed not conditional. But then I'm not so sure it's a good idea to mark it simp (because it prevents lemmas like bar (foo ⁻¹' X) ↔ baz X from triggering).
There was a problem hiding this comment.
Don't you mean lemmas like bar ⁻¹' (foo ⁻¹' X) ↔ baz X with ⁻¹' twice? Do we have any of those?
There was a problem hiding this comment.
Either way, I guess its out of scope for this PR.
|
bors merge |
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
