mathlib3 documentation

core / init.function

General operations on functions #

@[reducible]
def function.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β φ) (g : α β) :
α φ

Composition of functions: (f ∘ g) x = f (g x).

Equations
  • f g = λ (x : α), f (g x)
@[reducible]
def function.dcomp {α : Sort u₁} {β : α Sort u₂} {φ : Π {x : α}, β x Sort u₃} (f : Π {x : α} (y : β x), φ y) (g : Π (x : α), β x) (x : α) :
φ (g x)

Composition of dependent functions: (f ∘' g) x = f (g x), where type of g x depends on x and type of f (g x) depends on x and g x.

Equations
  • f ∘' g = λ (x : α), f (g x)
@[reducible]
def function.comp_right {α : Sort u₁} {β : Sort u₂} (f : β β β) (g : α β) :
β α β
Equations
@[reducible]
def function.comp_left {α : Sort u₁} {β : Sort u₂} (f : β β β) (g : α β) :
α β β
Equations
@[reducible]
def function.on_fun {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β β φ) (g : α β) :
α α φ

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
  • (f on g) = λ (x y : α), f (g x) (g y)
@[reducible]
def function.combine {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₁} (f : α β φ) (op : φ δ ζ) (g : α β δ) :
α β ζ
Equations
  • (f -[op]- g) = λ (x : α) (y : β), op (f x y) (g x y)
@[reducible]
def function.const {α : Sort u₁} (β : Sort u₂) (a : α) :
β α

Constant λ _, a.

Equations
@[reducible]
def function.swap {α : Sort u₁} {β : Sort u₂} {φ : α β Sort u₃} (f : Π (x : α) (y : β), φ x y) (y : β) (x : α) :
φ x y
Equations
@[reducible]
def function.app {α : Sort u₁} {β : α Sort u₂} (f : Π (x : α), β x) (x : α) :
β x
Equations
theorem function.left_id {α : Sort u₁} {β : Sort u₂} (f : α β) :
id f = f
theorem function.right_id {α : Sort u₁} {β : Sort u₂} (f : α β) :
f id = f
@[simp]
theorem function.comp_app {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β φ) (g : α β) (a : α) :
(f g) a = f (g a)
theorem function.comp.assoc {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} (f : φ δ) (g : β φ) (h : α β) :
(f g) h = f g h
@[simp]
theorem function.comp.left_id {α : Sort u₁} {β : Sort u₂} (f : α β) :
id f = f
@[simp]
theorem function.comp.right_id {α : Sort u₁} {β : Sort u₂} (f : α β) :
f id = f
theorem function.comp_const_right {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β φ) (b : β) :
def function.injective {α : Sort u₁} {β : Sort u₂} (f : α β) :
Prop

A function f : α → β is called injective if f x = f y implies x = y.

Equations
Instances for function.injective
theorem function.injective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : β φ} {f : α β} (hg : function.injective g) (hf : function.injective f) :
@[reducible]
def function.surjective {α : Sort u₁} {β : Sort u₂} (f : α β) :
Prop

A function f : α → β is called surjective if every b : β is equal to f a for some a : α.

Equations
theorem function.surjective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : β φ} {f : α β} (hg : function.surjective g) (hf : function.surjective f) :
def function.bijective {α : Sort u₁} {β : Sort u₂} (f : α β) :
Prop

A function is called bijective if it is both injective and surjective.

Equations
Instances for function.bijective
theorem function.bijective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : β φ} {f : α β} :
def function.left_inverse {α : Sort u₁} {β : Sort u₂} (g : β α) (f : α β) :
Prop

left_inverse g f means that g is a left inverse to f. That is, g ∘ f = id.

Equations
Instances for function.left_inverse
def function.has_left_inverse {α : Sort u₁} {β : Sort u₂} (f : α β) :
Prop

has_left_inverse f means that f has an unspecified left inverse.

Equations
def function.right_inverse {α : Sort u₁} {β : Sort u₂} (g : β α) (f : α β) :
Prop

right_inverse g f means that g is a right inverse to f. That is, f ∘ g = id.

Equations
Instances for function.right_inverse
def function.has_right_inverse {α : Sort u₁} {β : Sort u₂} (f : α β) :
Prop

has_right_inverse f means that f has an unspecified right inverse.

Equations
theorem function.left_inverse.injective {α : Sort u₁} {β : Sort u₂} {g : β α} {f : α β} :
theorem function.right_inverse_of_injective_of_left_inverse {α : Sort u₁} {β : Sort u₂} {f : α β} {g : β α} (injf : function.injective f) (lfg : function.left_inverse f g) :
theorem function.right_inverse.surjective {α : Sort u₁} {β : Sort u₂} {f : α β} {g : β α} (h : function.right_inverse g f) :
theorem function.left_inverse_of_surjective_of_right_inverse {α : Sort u₁} {β : Sort u₂} {f : α β} {g : β α} (surjf : function.surjective f) (rfg : function.right_inverse f g) :
def function.curry {α : Type u₁} {β : Type u₂} {φ : Type u₃} :
× β φ) α β φ

Interpret a function on α × β as a function with two arguments.

Equations
def function.uncurry {α : Type u₁} {β : Type u₂} {φ : Type u₃} :
β φ) α × β φ

Interpret a function with two arguments as a function on α × β

Equations
@[simp]
theorem function.curry_uncurry {α : Type u₁} {β : Type u₂} {φ : Type u₃} (f : α β φ) :
@[simp]
theorem function.uncurry_curry {α : Type u₁} {β : Type u₂} {φ : Type u₃} (f : α × β φ) :
@[protected]
theorem function.left_inverse.id {α : Type u₁} {β : Type u₂} {g : β α} {f : α β} (h : function.left_inverse g f) :
g f = id
@[protected]
theorem function.right_inverse.id {α : Type u₁} {β : Type u₂} {g : β α} {f : α β} (h : function.right_inverse g f) :
f g = id