Zulip Chat Archive
Stream: general
Topic: image of complement
Patrick Massot (Mar 13 2018 at 14:03):
Do we have {α : Type*} {β : Type*} (f : α ≃ β) (s : set α) : f '' -s = -(f '' s) in mathlib?
Johannes Hölzl (Mar 13 2018 at 14:05):
I guess you want f : A -> B, its preimage_compl.
Patrick Massot (Mar 13 2018 at 14:09):
No, I'd like what I stated
Patrick Massot (Mar 13 2018 at 14:09):
with direct image
Patrick Massot (Mar 13 2018 at 14:09):
assuming bijectivity
Patrick Massot (Mar 13 2018 at 14:10):
I admit both the equiv and double apostrophes are hard to read on my screen too
Kevin Buzzard (Mar 13 2018 at 14:11):
you could use preimage_compl on the map in the other direction ;-)
Patrick Massot (Mar 13 2018 at 14:12):
I'm pretty sure I can prove this lemma, I was asking about its current existence
Johannes Hölzl (Mar 13 2018 at 14:18):
Ah sorry. Then no: I think its not yet in mathlib.
Patrick Massot (Mar 13 2018 at 14:18):
Ok, I hope I'll be able to contribute this
Last updated: Dec 20 2023 at 11:08 UTC