Miscellaneous function constructions and lemmas #
If the co-domain
β of an injective function
f : α → β has decidable equality, then
α also has decidable equality.
g is a partial inverse to
f (an injective but not necessarily
surjective function) if
g y = some x implies
f x = y, and
g y = none
y is not in the range of
We can use choice to construct explicitly a partial inverse for
a given injective function
Construct the inverse for a function
f on domain
s. This function is a right inverse of
f '' s. For a computable version, see
Non-dependent version of
extend f g e' extends a function
g : α → γ
along a function
f : α → β to a function
β → γ,
by using the values of
g on the range of
and the values of an auxiliary function
e' : β → γ elsewhere.
Mostly useful when
f is injective.
Compose a binary function
f with a pair of unary functions
If both arguments of
f have the same type and
g = h, then
bicompl f g g = f on g.
- uncurry : α → β → γ
Records a way to turn an element of
α into a function from
γ. The most generic use
is to recursively uncurry. For instance
f : α → β → γ → δ will be turned into
↿f : α × β × γ → δ. One can also add instances for bundled maps.
The property of a binary function
f : α → β → γ being injective.
Mathematically this should be thought of as the corresponding function
α × β → γ being injective.
sometimes f evaluates to some value of
f, if it exists. This function is especially
interesting in the case where
α is a proposition, in which case
f is necessarily a
constant function, so that
sometimes f = f a for all
Note these lemmas apply to
Sort*, as the latter interferes with
is trivial anyway.
A set of functions "separates points strongly" if for each pair of distinct points there is a function with specified values on them.