General operations on functions #
Composition of functions:
(f ∘ g) x = f (g x).
- f ∘ g = λ (x : α), f (g x)
Composition of dependent functions:
(f ∘' g) x = f (g x), where type of
g x depends on
and type of
f (g x) depends on
- f ∘' g = λ (x : α), f (g x)
f : β → β → φ and
g : α → β, produce a function
α → α → φ that evaluates
g on each argument, then applies
f to the results. Can be used, e.g., to transfer a relation
- (f on g) = λ (x y : α), f (g x) (g y)
- (f -[op]- g) = λ (x : α) (y : β), op (f x y) (g x y)
λ _, a.
f : α → β is called injective if
f x = f y implies
x = y.
f : α → β is called surjective if every
b : β is equal to
a : α.
A function is called bijective if it is both injective and surjective.
left_inverse g f means that g is a left inverse to f. That is,
g ∘ f = id.
has_left_inverse f means that
f has an unspecified left inverse.
right_inverse g f means that g is a right inverse to f. That is,
f ∘ g = id.
has_right_inverse f means that
f has an unspecified right inverse.
Interpret a function on
α × β as a function with two arguments.
Interpret a function with two arguments as a function on
α × β