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 : α} → β x → Sort 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.

Equations

(f ∘' g) x = f x (g x)

Instances For

def Function.«term_∘'_» :

Lean.TrailingParserDescr

Equations

Function.«term_∘'_» = Lean.ParserDescr.trailingNode `Function.term_∘'_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘' ") (Lean.ParserDescr.cat `term 80))

Instances For

@[reducible]

def Function.compRight {α : Sort u₁} {β : Sort u₂} (f : β → β → β) (g : α → β) :

β → α → β

Equations

Function.compRight f g b a = f b (g a)

Instances For

@[reducible]

def Function.compLeft {α : Sort u₁} {β : Sort u₂} (f : β → β → β) (g : α → β) :

α → β → β

Equations

Function.compLeft f g a b = f (g a) b

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

Equations

(f on g) x y = f (g x) (g y)

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.

Equations

Function.combine f op g x y = op (f x y) (g x y)

Instances For

@[reducible]

def Function.swap {α : Sort u₁} {β : Sort u₂} {φ : α → β → Sort u₃} (f : (x : α) → (y : β) → φ x y) (y : β) (x : α) :

φ x y

Equations

Function.swap f y x = f x y

Instances For

@[reducible]

def Function.app {α : Sort u₁} {β : α → Sort u₂} (f : (x : α) → β x) (x : α) :

β x

Equations

Function.app f x = f x

Instances For

def Function.term_On_ :

Lean.TrailingParserDescr

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))

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

Equations

Function.Injective f = ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂

Instances For

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

Function.Injective (g ∘ f)

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

Equations

Function.Surjective f = ∀ (b : β), ∃ a, f a = b

Instances For

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

Function.Surjective (g ∘ f)

def Function.Bijective {α : Sort u₁} {β : Sort u₂} (f : α → β) :

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

Equations

Function.Bijective f = (Function.Injective f ∧ Function.Surjective f)

Instances For

theorem Function.Bijective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : β → φ} {f : α → β} :

Function.Bijective g → Function.Bijective 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.

Equations

Function.LeftInverse g f = ∀ (x : α), g (f x) = x

Instances For

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

HasLeftInverse f means that f has an unspecified left inverse.

Equations

Function.HasLeftInverse f = ∃ finv, Function.LeftInverse finv f

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.

Equations

Function.RightInverse g f = Function.LeftInverse f g

Instances For

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

HasRightInverse f means that f has an unspecified right inverse.

Equations

Function.HasRightInverse f = ∃ finv, Function.RightInverse finv f

Instances For

theorem Function.LeftInverse.injective {α : Sort u₁} {β : Sort u₂} {g : β → α} {f : α → β} :

Function.LeftInverse g f → Function.Injective f

theorem Function.HasLeftInverse.injective {α : Sort u₁} {β : Sort u₂} {f : α → β} :

Function.HasLeftInverse f → Function.Injective f

theorem Function.rightInverse_of_injective_of_leftInverse {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α} (injf : Function.Injective f) (lfg : Function.LeftInverse f g) :

Function.RightInverse f g

theorem Function.RightInverse.surjective {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α} (h : Function.RightInverse g f) :

Function.Surjective f

theorem Function.HasRightInverse.surjective {α : Sort u₁} {β : Sort u₂} {f : α → β} :

Function.HasRightInverse f → Function.Surjective f

theorem Function.leftInverse_of_surjective_of_rightInverse {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α} (surjf : Function.Surjective f) (rfg : Function.RightInverse f g) :

Function.LeftInverse f g

theorem Function.injective_id {α : Sort u₁} :

Function.Injective id

theorem Function.surjective_id {α : Sort u₁} :

Function.Surjective id

theorem Function.bijective_id {α : Sort u₁} :

Function.Bijective id

@[inline]

def Function.curry {α : Type u₁} {β : Type u₂} {φ : Type u₃} :

(α × β → φ) → α → β → φ

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

Equations

Function.curry f a b = f (a, b)

Instances For

@[inline]

def Function.uncurry {α : Type u₁} {β : Type u₂} {φ : Type u₃} :

(α → β → φ) → α × β → φ

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

Equations

Function.uncurry f a = f a.fst a.snd

Instances For

@[simp]

theorem Function.curry_uncurry {α : Type u₁} {β : Type u₂} {φ : Type u₃} (f : α → β → φ) :

Function.curry (Function.uncurry f) = f

@[simp]

theorem Function.uncurry_curry {α : Type u₁} {β : Type u₂} {φ : Type u₃} (f : α × β → φ) :

Function.uncurry (Function.curry f) = f

theorem Function.LeftInverse.id {α : Type u₁} {β : Type u₂} {g : β → α} {f : α → β} (h : Function.LeftInverse g f) :

g ∘ f = id

theorem Function.RightInverse.id {α : Type u₁} {β : Type u₂} {g : β → α} {f : α → β} (h : Function.RightInverse g f) :

f ∘ g = id