General operations on functions #
Composition of dependent functions: (f ∘' g) x = f (g x)
, where type of g x
depends on x
and type of f (g x)
depends on x
and g x
.
Instances For
Instances For
Instances For
Given functions 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
from β
to α
.
Instances For
Given functions f : α → β → φ
, g : α → β → δ
and a binary operator op : φ → δ → ζ
,
produce a function α → β → ζ
that applies f
and g
on each argument and then applies
op
to the results.
Instances For
Instances For
Instances For
Given functions 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
from β
to α
.
Instances For
A function f : α → β
is called injective if f x = f y
implies x = y
.
Instances For
A function f : α → β
is called surjective if every b : β
is equal to f a
for some a : α
.
Instances For
A function is called bijective if it is both injective and surjective.
Instances For
LeftInverse g f
means that g is a left inverse to f. That is, g ∘ f = id
.
Instances For
HasLeftInverse f
means that f
has an unspecified left inverse.
Instances For
RightInverse g f
means that g is a right inverse to f. That is, f ∘ g = id
.
Instances For
HasRightInverse f
means that f
has an unspecified right inverse.