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
- function.eval x f = f x
If the co-domain β
of an injective function f : α → β
has decidable equality, then
the domain α
also has decidable equality.
Equations
- I.decidable_eq = λ (a b : α), decidable_of_iff (f a = f b) _
Composition by an injective function on the left is itself injective.
Equations
- function.decidable_eq_pfun p α f g = decidable_of_iff (∀ (hp : p), f hp = g hp) _
Shorthand for using projection notation with function.bijective_iff_exists_unique
.
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 u
. This theorem
demonstrates why Type : Type
would be inconsistent in Lean.
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
implies that y
is not in the range of f
.
Equations
- function.is_partial_inv f g = ∀ (x : α) (y : β), g y = option.some x ↔ f x = y
We can use choice to construct explicitly a partial inverse for
a given injective function f
.
Equations
- function.partial_inv f b = dite (∃ (a : α), f a = b) (λ (h : ∃ (a : α), f a = b), option.some (classical.some h)) (λ (h : ¬∃ (a : α), f a = b), option.none)
The inverse of a function (which is a left inverse if f
is injective
and a right inverse if f
is surjective).
Equations
- function.inv_fun f = λ (y : β), dite (∃ (x : α), f x = y) (λ (h : ∃ (x : α), f x = y), h.some) (λ (h : ¬∃ (x : α), f x = y), classical.arbitrary α)
The inverse of a surjective function. (Unlike inv_fun
, this does not require
α
to be inhabited.)
Equations
- function.surj_inv h b = classical.some _
Composition by an surjective function on the left is itself surjective.
Composition by an bijective function on the left is itself bijective.
Replacing the value of a function at a given point by a given value.
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.
Equations
- function.extend f g e' = λ (b : β), dite (∃ (a : α), f a = b) (λ (h : ∃ (a : α), f a = b), g (classical.some h)) (λ (h : ¬∃ (a : α), f a = b), e' b)
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
- function.bicompl f g h a b = f (g a) (h b)
Instances for function.bicompl
Compose an unary function f
with a binary function g
.
Equations
- function.bicompr f g a b = f (g a b)
Instances for function.bicompr
- uncurry : α → β → γ
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 of this typeclass
Instances of other typeclasses for function.has_uncurry
- function.has_uncurry.has_sizeof_inst
Equations
- function.has_uncurry_base = {uncurry := id (α → β)}
A function is involutive, if f ∘ f = id
.
Equations
- function.involutive f = ∀ (x : α), f (f x) = x
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
.
The property of a binary function f : α → β → γ
being injective.
Mathematically this should be thought of as the corresponding function α × β → γ
being injective.
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.
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 a
.
Equations
- function.sometimes f = dite (nonempty α) (λ (h : nonempty α), f (classical.choice h)) (λ (h : ¬nonempty α), classical.choice _inst_1)
Note these lemmas apply to Type*
not Sort*
, as the latter interferes with simp
, and
is trivial anyway.
A set of functions "separates points" if for each pair of distinct points there is a function taking different values on them.
Equations
- A.separates_points = ∀ ⦃x y : α⦄, x ≠ y → (∃ (f : α → β) (H : f ∈ A), f x ≠ f y)