# Documentation

Mathlib.Init.Function

# General operations on functions #

theorem Function.comp_def {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} (f : βδ) (g : αβ) :
f g = fun x => f (g x)
@[inline, reducible]
def Function.dcomp {α : Sort u₁} {β : αSort u₂} {φ : {x : α} → β xSort u₃} (f : {x : α} → (y : β x) → φ x y) (g : (x : α) → β 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.

Instances For
Instances For
@[reducible]
def Function.compRight {α : Sort u₁} {β : Sort u₂} (f : βββ) (g : αβ) :
βαβ
Instances For
@[reducible]
def Function.compLeft {α : Sort u₁} {β : Sort u₂} (f : βββ) (g : αβ) :
αββ
Instances For
@[reducible]
def Function.onFun {α : 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 α.

Instances For
@[reducible]
def Function.combine {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₅} (f : αβφ) (op : φδζ) (g : αβδ) :
αβζ

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.

Instances For
@[reducible]
def Function.swap {α : Sort u₁} {β : Sort u₂} {φ : αβSort u₃} (f : (x : α) → (y : β) → φ x y) (y : β) (x : α) :
φ x y
Instances For
@[reducible]
def Function.app {α : Sort u₁} {β : αSort u₂} (f : (x : α) → β x) (x : α) :
β x
Instances For

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 α.

Instances For
theorem Function.left_id {α : Sort u₁} {β : Sort u₂} (f : αβ) :
id f = f
theorem Function.right_id {α : Sort u₁} {β : Sort u₂} (f : αβ) :
f id = f
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 : β) :
f = Function.const α (f b)
def Function.Injective {α : Sort u₁} {β : Sort u₂} (f : αβ) :

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

Instances For
theorem Function.Injective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : βφ} {f : αβ} (hg : ) (hf : ) :
def Function.Surjective {α : Sort u₁} {β : Sort u₂} (f : αβ) :

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

Instances For
theorem Function.Surjective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : βφ} {f : αβ} (hg : ) (hf : ) :
def Function.Bijective {α : Sort u₁} {β : Sort u₂} (f : αβ) :

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

Instances For
theorem Function.Bijective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : βφ} {f : αβ} :
Function.Bijective (g f)
def Function.LeftInverse {α : Sort u₁} {β : Sort u₂} (g : βα) (f : αβ) :

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

Instances For
def Function.HasLeftInverse {α : Sort u₁} {β : Sort u₂} (f : αβ) :

HasLeftInverse f means that f has an unspecified left inverse.

Instances For
def Function.RightInverse {α : Sort u₁} {β : Sort u₂} (g : βα) (f : αβ) :

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

Instances For
def Function.HasRightInverse {α : Sort u₁} {β : Sort u₂} (f : αβ) :

HasRightInverse f means that f has an unspecified right inverse.

Instances For
theorem Function.LeftInverse.injective {α : Sort u₁} {β : Sort u₂} {g : βα} {f : αβ} :
theorem Function.HasLeftInverse.injective {α : Sort u₁} {β : Sort u₂} {f : αβ} :
theorem Function.rightInverse_of_injective_of_leftInverse {α : Sort u₁} {β : Sort u₂} {f : αβ} {g : βα} (injf : ) (lfg : ) :
theorem Function.RightInverse.surjective {α : Sort u₁} {β : Sort u₂} {f : αβ} {g : βα} (h : ) :
theorem Function.HasRightInverse.surjective {α : Sort u₁} {β : Sort u₂} {f : αβ} :
theorem Function.leftInverse_of_surjective_of_rightInverse {α : Sort u₁} {β : Sort u₂} {f : αβ} {g : βα} (surjf : ) (rfg : ) :
theorem Function.injective_id {α : Sort u₁} :
theorem Function.surjective_id {α : Sort u₁} :
theorem Function.bijective_id {α : Sort u₁} :
@[inline]
def Function.curry {α : Type u₁} {β : Type u₂} {φ : Type u₃} :
(α × βφ) → αβφ

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

Instances For
@[inline]
def Function.uncurry {α : Type u₁} {β : Type u₂} {φ : Type u₃} :
(αβφ) → α × βφ

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

Instances For
@[simp]
theorem Function.curry_uncurry {α : Type u₁} {β : Type u₂} {φ : Type u₃} (f : αβφ) :
@[simp]
theorem Function.uncurry_curry {α : Type u₁} {β : Type u₂} {φ : Type u₃} (f : α × βφ) :
theorem Function.LeftInverse.id {α : Type u₁} {β : Type u₂} {g : βα} {f : αβ} (h : ) :
g f = id
theorem Function.RightInverse.id {α : Type u₁} {β : Type u₂} {g : βα} {f : αβ} (h : ) :
f g = id