General operations on functions #
Equations
- Function.comp_right f g b a = f b (g a)
Equations
- Function.comp_left f g a b = f (g a) b
Given functions f : β → β → φ→ β → φ→ φ
and g : α → β→ β
, produce a function α → α → φ→ α → φ→ φ
that evaluates
g
on each argument, then applies f
to the results. Can be used, e.g., to transfer a relation
from β
to α
.
Given functions f : α → β → φ→ β → φ→ φ
, g : α → β → δ→ β → δ→ δ
and a binary operator op : φ → δ → ζ→ δ → ζ→ ζ
,
produce a function α → β → ζ→ β → ζ→ ζ
that applies f
and g
on each argument and then applies
op
to the results.
Equations
- Function.combine f op g x y = op (f x y) (g x y)
Equations
- Function.swap f y x = f x y
Equations
- Function.app f x = f x
Given functions f : β → β → φ→ β → φ→ φ
and g : α → β→ β
, produce a function α → α → φ→ α → φ→ φ
that evaluates
g
on each argument, then applies f
to the results. Can be used, e.g., to transfer a relation
from β
to α
.
Equations
- Function.term_On_ = Lean.ParserDescr.trailingNode `Function.term_On_ 2 2 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " on ") (Lean.ParserDescr.cat `term 3))
A function f : α → β→ β
is called injective if f x = f y
implies x = y
.
Equations
- Function.Injective f = ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
A function f : α → β→ β
is called surjective if every b : β
is equal to f a
for some a : α
.
Equations
- Function.Surjective f = ∀ (b : β), ∃ a, f a = b
A function is called bijective if it is both injective and surjective.
Equations
LeftInverse g f
means that g is a left inverse to f. That is, g ∘ f = id∘ f = id
.
Equations
- Function.LeftInverse g f = ∀ (x : α), g (f x) = x
HasLeftInverse f
means that f
has an unspecified left inverse.
Equations
- Function.HasLeftInverse f = ∃ finv, Function.LeftInverse finv f
RightInverse g f
means that g is a right inverse to f. That is, f ∘ g = id∘ g = id
.
Equations
hasRightInverse f
means that f
has an unspecified right inverse.
Equations
- Function.HasRightInverse f = ∃ finv, Function.RightInverse finv f
Interpret a function on α × β× β
as a function with two arguments.
Equations
- Function.curry f a b = f (a, b)
Interpret a function with two arguments as a function on α × β× β
Equations
- Function.uncurry f a = f a.fst a.snd