mathlib docs: core.init.function

def function.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} :

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

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

Equations

f ∘ g = λ (x : α), f (g x)

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)

source

def function.comp_right {α : Sort u₁} {β : Sort u₂} :

(β → β → β) → (α → β) → β → α → β

Equations

function.comp_right f g = λ (b : β) (a : α), f b (g a)

source

def function.comp_left {α : Sort u₁} {β : Sort u₂} :

(β → β → β) → (α → β) → α → β → β

Equations

function.comp_left f g = λ (a : α) (b : β), f (g a) b

source

def function.on_fun {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} :

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

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)

source

def function.combine {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₁} :

(α → β → φ) → (φ → δ → ζ) → (α → β → δ) → α → β → ζ

Equations

(f -[op]- g) = λ (x : α) (y : β), op (f x y) (g x y)

source

def function.const {α : Sort u₁} (β : Sort u₂) :

α → β → α

Constant λ _, a.

Equations

function.const β a = λ (x : β), a

source

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

source

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

β x

Equations

function.app f x = f x

source

theorem function.left_id {α : Sort u₁} {β : Sort u₂} (f : α → β) :

id ∘ f = f

source

theorem function.right_id {α : Sort u₁} {β : Sort u₂} (f : α → β) :

f ∘ id = f

source

@[simp]

theorem function.comp_app {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β → φ) (g : α → β) (a : α) :

(f ∘ g) a = f (g a)

source

theorem function.comp.assoc {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} (f : φ → δ) (g : β → φ) (h : α → β) :

(f ∘ g) ∘ h = f ∘ g ∘ h

source

@[simp]

theorem function.comp.left_id {α : Sort u₁} {β : Sort u₂} (f : α → β) :

id ∘ f = f

source

@[simp]

theorem function.comp.right_id {α : Sort u₁} {β : Sort u₂} (f : α → β) :

f ∘ id = f

source

theorem function.comp_const_right {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β → φ) (b : β) :

f ∘ function.const α b = function.const α (f b)

source

def function.injective {α : Sort u₁} {β : Sort u₂} :

(α → β) → Prop

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₂

source

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

function.injective g → function.injective f → function.injective (g ∘ f)

source

def function.surjective {α : Sort u₁} {β : Sort u₂} :

(α → β) → Prop

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

Equations

function.surjective f = ∀ (b : β), ∃ (a : α), f a = b

source

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

function.surjective g → function.surjective f → function.surjective (g ∘ f)

source

def function.bijective {α : Sort u₁} {β : Sort u₂} :

(α → β) → Prop

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

Equations

function.bijective f = (function.injective f ∧ function.surjective f)

source

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

function.bijective g → function.bijective f → function.bijective (g ∘ f)

source

def function.left_inverse {α : Sort u₁} {β : Sort u₂} :

(β → α) → (α → β) → Prop

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

Equations

function.left_inverse g f = ∀ (x : α), g (f x) = x

source

def function.has_left_inverse {α : Sort u₁} {β : Sort u₂} :

(α → β) → Prop

has_left_inverse f means that f has an unspecified left inverse.

Equations

function.has_left_inverse f = ∃ (finv : β → α), function.left_inverse finv f

source

def function.right_inverse {α : Sort u₁} {β : Sort u₂} :

(β → α) → (α → β) → Prop

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

Equations

function.right_inverse g f = function.left_inverse f g

source

def function.has_right_inverse {α : Sort u₁} {β : Sort u₂} :

(α → β) → Prop

has_right_inverse f means that f has an unspecified right inverse.

Equations

function.has_right_inverse f = ∃ (finv : β → α), function.right_inverse finv f

source

theorem function.left_inverse.injective {α : Sort u₁} {β : Sort u₂} {g : β → α} {f : α → β} :

function.left_inverse g f → function.injective f

source

theorem function.has_left_inverse.injective {α : Sort u₁} {β : Sort u₂} {f : α → β} :

function.has_left_inverse f → function.injective f

source

theorem function.right_inverse_of_injective_of_left_inverse {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α} :

function.injective f → function.left_inverse f g → function.right_inverse f g

source

theorem function.right_inverse.surjective {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α} :

function.right_inverse g f → function.surjective f

source

theorem function.has_right_inverse.surjective {α : Sort u₁} {β : Sort u₂} {f : α → β} :

function.has_right_inverse f → function.surjective f

source

theorem function.left_inverse_of_surjective_of_right_inverse {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α} :

function.surjective f → function.right_inverse f g → function.left_inverse f g

source

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

function.injective id

source

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

function.surjective id

source

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

function.bijective id

source

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)

source

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

source

@[simp]

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

function.curry (function.uncurry f) = f

source

@[simp]

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

function.uncurry (function.curry f) = f

source

theorem function.left_inverse.id {α : Type u₁} {β : Type u₂} {g : β → α} {f : α → β} :

function.left_inverse g f → g ∘ f = id

source

def function.right_inverse.id {α : Type u₁} {β : Type u₂} {g : β → α} {f : α → β} :

function.right_inverse g f → f ∘ g = id

Equations

_ = _

mathlib documentation

core.init.function

General operations on functions

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​function

General operations on functions

General documentation

Additional documentation

Library

core.init.function