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