The file init/function.lean in the core library has basic defintions
and facts about functions between general types.
comp (function composition), id (the identity function), const (a
constant function), injective,surjective,bijective. Note that many
of these things live in the function namespace, which has to be opened
first.
universes u variables (X Y Z : Type u)
variables (f : X → Y) (g : Y → Z) (h : Y → X)
open function
example : bijective g → bijective f → bijective (g ∘ f) := bijective_comp
example : has_left_inverse f → injective f := injective_of_has_left_inverse
example : left_inverse h f → h ∘ f = id := id_of_left_inverse