Library
▹
Essentials
▹
Functions
Definition 1.5.11.
Let
X
,
Y
,
Z
be sets,
f
:
X
→
Y
,
g
:
Y
→
Z
be
functions
. We define:
g
∘
f
:
X
→
Z
x
↦
g
(
f
(
x
))
References.
https://en.wikipedia.org/wiki/Function_composition
https://mathworld.wolfram.com/Composition.html
https://proofwiki.org/wiki/Definition:Composition_of_Mappings
https://ncatlab.org/nlab/show/composition
https://coq.inria.fr/library/Coq.Program.Basics.html#compose
https://leanprover-community.github.io/mathlib_docs/init/function.html#function.comp