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
Instances For
If the co-domain β of an injective function f : α → β has decidable equality, then
the domain α also has decidable equality.
Equations
- I.decidableEq x✝¹ x✝ = decidable_of_iff (f x✝¹ = f x✝) ⋯
Instances For
Equations
- Function.decidableEqPFun p α x✝¹ x✝ = decidable_of_iff (∀ (hp : p), x✝¹ hp = x✝ hp) ⋯
Shorthand for using projection notation with Function.bijective_iff_existsUnique.
If f : α → α → β is surjective, then every endofunction on β has a fixed point.
This is an instance of Lawvere's fixed-point theorem applied to the category of types
and functions. It is the diagonal argument underlying cantor_surjective and
cantor_injective.
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.
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.
Instances For
Alias of Function.IsPartialInv.eq.
Alias of Function.IsPartialInv.injective.
We can use choice to construct explicitly a partial inverse for
a given injective function f.
Equations
Instances For
Alias of Function.Injective.isPartialInv.
The inverse of a function (which is a left inverse if f is injective
and a right inverse if f is surjective).
Equations
- Function.invFun f y = if h : ∃ (x : α), f x = y then h.choose else Classical.arbitrary α
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
- Function.update f a' v a = if h : a = a' then ⋯ ▸ v else f a
Instances For
A congruence lemma for Function.update, specialized for the non-dependent case. Without this,
simp can't rewrite in the fourth argument a because the result type depends on a.
See also https://github.com/leanprover/lean4/issues/12478.
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
- Function.extend f g j b = if h : ∃ (a : α), f a = b then g (Classical.choose h) else j b
Instances For
g factors through f : f a = f b → g a = g b
Equations
- Function.FactorsThrough g f = ∀ ⦃a b : α⦄, f a = f b → g a = g b
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
- Function.«term↿_» = Lean.ParserDescr.node `Function.«term↿_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↿") (Lean.ParserDescr.cat `term 1024))
Instances For
Equations
- Function.hasUncurryBase = { uncurry := id }
A function is involutive, if f ∘ f = id.
Equations
- Function.Involutive f = ∀ (x : α), f (f x) = x
Instances For
An involution commutes across an equality. Compare to Function.Injective.eq_iff.
Alias of Function.symm_apply_eq_iff.
The property of a binary function f : α → β → γ being injective.
Mathematically this should be thought of as the corresponding function α × β → γ being injective.
Instances For
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 = if h : Nonempty α then f (Classical.choice h) else Classical.choice inst✝
Instances For
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.
Alias of Std.Symm.forall_existsUnique_iff'.
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.
Alias of Std.Symm.forall_existsUnique_iff.
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.
A set of functions "separates points" if for each pair of distinct points there is a function taking different values on them.