Zulip Chat Archive

Stream: new members

Topic: Restricting range of function


view this post on Zulip 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 → β

view this post on Zulip Kevin Buzzard (Jun 23 2020 at 14:58):

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

view this post on Zulip Reid Barton (Jun 23 2020 at 14:58):

Just by hand is probably easiest.

view this post on Zulip Reid Barton (Jun 23 2020 at 15:00):

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

view this post on Zulip 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