equiv_embedding_image

Stream: Is there code for X?

[Scott Morrison]

Where is

def blah {α β : Type*} (r : α ↪ β) (s : set α) : s ≃ r '' s := sorry

[Yaël Dillies]

There is docs#equiv.image

[Eric Wieser]

docs#equiv.set.image

[Eric Wieser]

I had an attempt to provide a computable version in #11347, but it's a pain to deal with "either has a left inverse or has an uninhabited domain"