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
.
Equations
Instances For
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
.
Equations
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 α
.
Equations
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 α
.
Equations
Instances For
A function f : α → β
is called injective if f x = f y
implies x = y
.
Equations
Instances For
A function f : α → β
is called surjective if every b : β
is equal to f a
for some a : α
.
Equations
Instances For
A function is called bijective if it is both injective and surjective.
Equations
Instances For
A point x
is a fixed point of f : α → α
if f x = x
.