Restriction of a bundled function to a subset

Stream: new members

[Luigi Massacci]

If I have some function f : X -> Y, is there a canonical way (maybe with the standard math notation too) to define the restriction f : S -> Y for some subset S of X?

[Riccardo Brasca]

We have docs#Set.restrict and docs#Subtype.restrict depending on your precise situation

[Luigi Massacci]

Second one I think is good. Thanks!

[Luigi Massacci]

Actually it doesn't quite work. My problem is that I have a bundled function type E(X). So fromf : E(X) I want to go to f' : E(S) (which I need to pass as hypothesis to a theorem). The restriction trivially satisfies the requirements for being E(S)) but if I just do Set.restrict I'm reasonably missing the proof parts. Do I just def my own restriction ? I see that is what is done for ContinuousMap.restrict

[Riccardo Brasca]

Can you write a #mwe?

[Riccardo Brasca]

But if your function is really bundled you have to write the def by hand I think (since there is a theorem behind the scene, maybe a trivial one, but still a theorem)

[Riccardo Brasca]

like docs#MonoidHom.restrict, that is done by hand.

[Riccardo Brasca]

(Note that here the point is to have docs#SubmonoidClass.subtype, that is the inclusion as a bundled hom, and of course compose with it)