Documentation

Mathlib.Init.Function

Note about `Mathlib/Init/` #

The files in Mathlib/Init are leftovers from the port from Mathlib3. (They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)

We intend to move all the content of these files out into the main Mathlib directory structure. Contributions assisting with this are appreciated.

#align statements without corresponding declarations (i.e. because the declaration is in Batteries or Lean) can be left here. These will be deleted soon so will not significantly delay deleting otherwise empty Init files.

General operations on functions #

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

flip f = fun (b : β) (a : α) => f a b

@[reducible, inline]

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)

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, deprecated]

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

β → α → β

Equations

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

Instances For

@[reducible, deprecated]

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

α → β → β

Equations

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

Instances For

@[reducible, inline]

abbrev 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

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

@[reducible, deprecated]

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, inline]

abbrev 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

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

Function.swap f = fun (y : β) (x : α) => f x y

@[reducible, deprecated]

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

β x

Equations

Function.app f x = f x

Instances For

@[simp]

theorem Function.id_comp {α : Sort u₁} {β : Sort u₂} (f : α → β) :

id ∘ f = f

@[deprecated Function.id_comp]

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

id ∘ f = f

Alias of Function.id_comp.

@[deprecated Function.id_comp]

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

id ∘ f = f

Alias of Function.id_comp.

@[simp]

theorem Function.comp_id {α : Sort u₁} {β : Sort u₂} (f : α → β) :

f ∘ id = f

@[deprecated Function.comp_id]

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

f ∘ id = f

Alias of Function.comp_id.

@[deprecated Function.comp_id]

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

f ∘ id = f

Alias of Function.comp_id.

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

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

@[simp]

theorem Function.const_comp {α : Sort u₁} {β : Sort u₂} {γ : Sort u_1} (f : α → β) (c : γ) :

Function.const β c ∘ f = Function.const α c

@[simp]

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

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

@[deprecated Function.comp_const]

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

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

Alias of Function.comp_const.

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