## Stream: new members

### Topic: Restricting range of function

#### Jason KY. (Jun 23 2020 at 14:57):

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 (Jun 23 2020 at 14:58):

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

#### Reid Barton (Jun 23 2020 at 14:58):

Just by hand is probably easiest.

#### Reid Barton (Jun 23 2020 at 15:00):

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

#### Jason KY. (Jun 23 2020 at 15:00):

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

Last updated: May 10 2021 at 00:31 UTC