Miscellaneous function constructions and lemmas #
Evaluate a function at an argument. Useful if you want to talk about the partially applied
Function.eval x : (∀ x, β x) → β x
.
Instances For
If the co-domain β
of an injective function f : α → β
has decidable equality, then
the domain α
also has decidable equality.
Instances For
Composition by an injective function on the left is itself injective.
Shorthand for using projection notation with Function.bijective_iff_existsUnique
.
Cantor's diagonal argument implies that there are no surjective functions from α
to Set α
.
Cantor's diagonal argument implies that there are no injective functions from Set α
to α
.
There is no surjection from α : Type u
into Type (max u v)
. This theorem
demonstrates why Type : Type
would be inconsistent in Lean.
We can use choice to construct explicitly a partial inverse for
a given injective function f
.
Instances For
The inverse of a function (which is a left inverse if f
is injective
and a right inverse if f
is surjective).
Instances For
The inverse of a surjective function. (Unlike invFun
, this does not require
α
to be inhabited.)
Instances For
Composition by a surjective function on the left is itself surjective.
Composition by a bijective function on the left is itself bijective.
Replacing the value of a function at a given point by a given value.
Instances For
On non-dependent functions, Function.update
can be expressed as an ite
Non-dependent version of Function.update_comp_eq_of_forall_ne'
Non-dependent version of Function.update_comp_eq_of_injective'
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 f
and the values of an auxiliary function e' : β → γ
elsewhere.
Mostly useful when f
is injective, or more generally when g.factors_through f
Instances For
Compose a binary function f
with a pair of unary functions g
and h
.
If both arguments of f
have the same type and g = h
, then bicompl f g g = f on g
.
Instances For
- uncurry : α → β → γ
Uncurrying operator. The most generic use is to recursively uncurry. For instance
f : α → β → γ → δ
will be turned into↿f : α × β × γ → δ
. One can also add instances for bundled maps.
Records a way to turn an element of α
into a function from β
to γ
. 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
A function is involutive, if f ∘ f = id
.
Instances For
Involuting an ite
of an involuted value x : α
negates the Prop
condition in the ite
.
An involution commutes across an equality. Compare to Function.Injective.eq_iff
.
A binary injective function is injective when only the left argument varies.
A binary injective function is injective when only the right argument varies.
As a map from the left argument to a unary function, f
is injective.
As a map from the right argument to a unary function, f
is injective.
Note these lemmas apply to Type*
not Sort*
, as the latter interferes with simp
, and
is trivial anyway.