Restricting range of function

Stream: new members

[Jason KY.]

Hi!
I have the following question:

import topology.metric_space.basic
variables {α β γ : Type*} {S : set α}
variables {f : α → β} {g : f '' S → γ}

I would like to make a function like (g ∘ f) : ↥S → γ. Is there a way to do this?
I've tried using set.restrict but I don't think that would work for this case #check set.restrict f S -- set.restrict f S : ↥S → β

[Kevin Buzzard]

I guess you could define f' : \a \to f '' S and compose that.

[Reid Barton]

Just by hand is probably easiest.

[Reid Barton]

Though, there is def image_factorization (f : α → β) (s : set α) : s → f '' s

[Jason KY.]

Yes, I think that is exactly what I'm looking for! Thanks!