Library
▹
Essentials
▹
Functions
Definition 1.5.10.
Let
X
be a set,
A
⊆
X
,
Y
be a set,
f
:
X
→
Y
be a
function
. We define:
f
∣
A
:
=
f
∣
A
Y
References.
https://en.wikipedia.org/wiki/Restriction_(mathematics)
https://proofwiki.org/wiki/Definition:Restriction/Mapping
https://ncatlab.org/nlab/show/restriction
https://leanprover-community.github.io/mathlib_docs/data/subtype.html#subtype.restrict