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
.
Equations
Instances For
If the co-domain β
of an injective function f : α → β
has decidable equality, then
the domain α
also has decidable equality.
Equations
Instances For
Equations
Shorthand for using projection notation with Function.bijective_iff_existsUnique
.
Cantor's diagonal argument implies that there are no surjective functions from α
to Set α
.
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
.
Equations
Instances For
The inverse of a function (which is a left inverse if f
is injective
and a right inverse if f
is surjective).
Equations
Instances For
The inverse of a surjective function. (Unlike invFun
, this does not require
α
to be inhabited.)
Equations
Instances For
Composition by a surjective function on the left is itself surjective.
Replacing the value of a function at a given point by a given value.
Equations
Instances For
Alias of Function.update_self
.
Alias of Function.update_of_ne
.
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'
Recursors can be pushed inside Function.update
.
The ctor
argument should be a one-argument constructor like Sum.inl
,
and recursor
should be an inductive recursor partially applied in all but that constructor,
such as (Sum.rec · g)
.
In future, we should build some automation to generate applications like Option.rec_update
for all
inductive types.
Extension of a function g : α → γ
along a function f : α → β
.
For every a : α
, f a
is sent to g a
. f
might not be surjective, so we use an auxiliary
function j : β → γ
by sending b : β
not in the range of f
to j b
. If you do not care about
the behavior outside the range, j
can be used as a junk value by setting it to be 0
or
Classical.arbitrary
(assuming γ
is nonempty).
This definition is mathematically meaningful only when f a₁ = f a₂ → g a₁ = g a₂
(spelled
g.FactorsThrough f
). In particular this holds if f
is injective.
A typical use case is extending a function from a subtype to the entire type. If you wish to extend
g : {b : β // p b} → γ
to a function β → γ
, you should use Function.extend Subtype.val g j
.
Equations
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
.
Equations
Instances For
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.
- 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.
Instances
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.
Equations
Instances For
Equations
Equations
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.
A relation r : α → β → Prop
is "function-like"
(for each a
there exists a unique b
such that r a b
)
if and only if it is (f · = ·)
for some function f
.
A relation r : α → β → Prop
is "function-like"
(for each a
there exists a unique b
such that r a b
)
if and only if it is (f · = ·)
for some function f
.
A symmetric relation r : α → α → Prop
is "function-like"
(for each a
there exists a unique b
such that r a b
)
if and only if it is (f · = ·)
for some involutive function f
.
A symmetric relation r : α → α → Prop
is "function-like"
(for each a
there exists a unique b
such that r a b
)
if and only if it is (f · = ·)
for some involutive function f
.
Note these lemmas apply to Type*
not Sort*
, as the latter interferes with simp
, and
is trivial anyway.