Miscellaneous function constructions and lemmas #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
The inverse of a function (which is a left inverse if
f is injective
and a right inverse if
f is surjective).
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, more generally when
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.
Compose an unary function
f with a binary function
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.
Instances of this typeclass
Instances of other typeclasses for
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.