doc-next-gen

Mathlib.Logic.Function.Defs

Module docstring

{"# General operations on functions "}

Function.flip_def theorem
{f : α → β → φ} : flip f = fun b a => f a b
Full source 
lemma flip_def {f : α → β → φ} : flip f = fun b a => f a b := rfl
Definition of Function Flipping: $\mathrm{flip}\, f = \lambda b\, a, f\, a\, b$
Informal description
For any function $f \colon \alpha \to \beta \to \phi$, the flipped version of $f$, denoted as $\mathrm{flip}\, f$, is equal to the function $\lambda b\, a, f\, a\, b$.
Function.dcomp definition
{β : α → Sort u₂} {φ : ∀ {x : α}, β x → Sort u₃} (f : ∀ {x : α} (y : β x), φ y) (g : ∀ x, β x) : ∀ x, φ (g x)
Full source 
/-- 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`. -/
@[inline, reducible]
def dcomp {β : α → Sort u₂} {φ : ∀ {x : α}, β x → Sort u₃} (f : ∀ {x : α} (y : β x), φ y)
    (g : ∀ x, β x) : ∀ x, φ (g x) := fun x => f (g x)
Dependent function composition
Informal description
Given a type family $\beta$ depending on $\alpha$ and a type family $\varphi$ depending on $\beta$, the dependent composition of functions $f$ and $g$ is defined as $(f \circ' g)(x) = f(g(x))$ for each $x \in \alpha$, where $f$ takes an argument $y$ of type $\beta(x)$ and returns a value in $\varphi(y)$, and $g$ maps each $x$ to a value in $\beta(x)$.
Function.term_∘'_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixr:80 " ∘' " => Function.dcomp
Dependent function composition
Informal description
The notation `∘'` represents the dependent composition of functions. Given functions `f : ∀ {x : α}, β x → φ x` and `g : ∀ x, β x`, the composition `f ∘' g` is defined as the function mapping each `x : α` to `f (g x)`.
Function.onFun abbrev
(f : β → β → φ) (g : α → β) : α → α → φ
Full source 
/-- 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 `α`. -/
abbrev onFun (f : β → β → φ) (g : α → β) : α → α → φ := fun x y => f (g x) (g y)
Binary Function Composition via Unary Function (`f` on `g`)
Informal description
Given a binary function $f \colon \beta \to \beta \to \phi$ and a function $g \colon \alpha \to \beta$, the operation `onFun` produces a binary function $\alpha \to \alpha \to \phi$ that applies $g$ to both arguments and then applies $f$ to the results. That is, for any $x, y \in \alpha$, the resulting function is defined as: \[ \text{onFun}(f, g)(x, y) = f(g(x), g(y)). \] This can be used, for example, to transfer a relation from $\beta$ to $\alpha$ via $g$.
Function.term_On_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc onFun]
scoped infixl:2 " on " => onFun
`on` operator for function composition
Informal description
The infix notation `on` is defined for the function `onFun`, which takes a binary operation `f : β → β → φ` and a function `g : α → β`, and produces a new binary operation `α → α → φ` by applying `g` to both arguments before passing them to `f`. The notation is left-associative with precedence level 2.
Function.swap abbrev
{φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : ∀ y x, φ x y
Full source 
/-- For a two-argument function `f`, `swap f` is the same function but taking the arguments
in the reverse order. `swap f y x = f x y`. -/
abbrev swap {φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : ∀ y x, φ x y := fun y x => f x y
Function Argument Swapping
Informal description
For a two-argument function $f : \alpha \to \beta \to \gamma$, the swapped version $\operatorname{swap} f$ is defined as the function that takes its arguments in reverse order, i.e., $\operatorname{swap} f\, y\, x = f\, x\, y$ for all $x \in \alpha$ and $y \in \beta$.
Function.swap_def theorem
{φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : swap f = fun y x => f x y
Full source 
theorem swap_def {φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : swap f = fun y x => f x y := rfl
Definition of Function Argument Swapping: $\operatorname{swap} f = \lambda y\, x, f\, x\, y$
Informal description
For any two-argument function $f \colon \alpha \to \beta \to \gamma$, the swapped function $\operatorname{swap} f$ is equal to the function that reverses the order of its arguments, i.e., $\operatorname{swap} f = \lambda y\, x, f\, x\, y$.
Function.id_comp theorem
(f : α → β) : id ∘ f = f
Full source 
@[simp, mfld_simps]
theorem id_comp (f : α → β) : idid ∘ f = f := rfl
Identity Function Composition: $\mathrm{id} \circ f = f$
Informal description
For any function $f \colon \alpha \to \beta$, the composition of the identity function with $f$ equals $f$, i.e., $\mathrm{id} \circ f = f$.
Function.comp_id theorem
(f : α → β) : f ∘ id = f
Full source 
@[simp, mfld_simps]
theorem comp_id (f : α → β) : f ∘ id = f := rfl
Right Identity Property of Function Composition
Informal description
For any function $f \colon \alpha \to \beta$, the composition of $f$ with the identity function $\mathrm{id}$ is equal to $f$, i.e., $f \circ \mathrm{id} = f$.
Function.comp_assoc theorem
(f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘ h = f ∘ g ∘ h
Full source 
theorem comp_assoc (f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘ h = f ∘ g ∘ h :=
  rfl
Associativity of Function Composition: $(f \circ g) \circ h = f \circ (g \circ h)$
Informal description
For any functions $f \colon \phi \to \delta$, $g \colon \beta \to \phi$, and $h \colon \alpha \to \beta$, the composition $(f \circ g) \circ h$ is equal to $f \circ (g \circ h)$.
Function.Injective definition
(f : α → β) : Prop
Full source 
/-- A function `f : α → β` is called injective if `f x = f y` implies `x = y`. -/
def Injective (f : α → β) : Prop :=
  ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
Injective function
Informal description
A function \( f : \alpha \to \beta \) is called injective if for any \( a_1, a_2 \in \alpha \), \( f(a_1) = f(a_2) \) implies \( a_1 = a_2 \).
Function.Injective.comp theorem
{g : β → φ} {f : α → β} (hg : Injective g) (hf : Injective f) : Injective (g ∘ f)
Full source 
theorem Injective.comp {g : β → φ} {f : α → β} (hg : Injective g) (hf : Injective f) :
    Injective (g ∘ f) := fun _a₁ _a₂ => fun h => hf (hg h)
Composition of Injective Functions is Injective
Informal description
Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \phi$ be injective functions. Then the composition $g \circ f \colon \alpha \to \phi$ is also injective.
Function.Surjective definition
(f : α → β) : Prop
Full source 
/-- A function `f : α → β` is called surjective if every `b : β` is equal to `f a`
for some `a : α`. -/
def Surjective (f : α → β) : Prop :=
  ∀ b, ∃ a, f a = b
Surjective function
Informal description
A function \( f : \alpha \to \beta \) is called surjective if for every \( b \in \beta \), there exists an \( a \in \alpha \) such that \( f(a) = b \).
Function.Surjective.comp theorem
{g : β → φ} {f : α → β} (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f)
Full source 
theorem Surjective.comp {g : β → φ} {f : α → β} (hg : Surjective g) (hf : Surjective f) :
    Surjective (g ∘ f) := fun c : φ =>
  Exists.elim (hg c) fun b hb =>
    Exists.elim (hf b) fun a ha =>
      Exists.intro a (show g (f a) = c from Eq.trans (congr_arg g ha) hb)
Composition of Surjective Functions is Surjective
Informal description
Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \varphi$ be surjective functions. Then the composition $g \circ f \colon \alpha \to \varphi$ is also surjective.
Function.Bijective definition
(f : α → β)
Full source 
/-- A function is called bijective if it is both injective and surjective. -/
def Bijective (f : α → β) :=
  InjectiveInjective f ∧ Surjective f
Bijective function
Informal description
A function \( f : \alpha \to \beta \) is called bijective if it is both injective (for any \( a_1, a_2 \in \alpha \), \( f(a_1) = f(a_2) \) implies \( a_1 = a_2 \)) and surjective (for every \( b \in \beta \), there exists an \( a \in \alpha \) such that \( f(a) = b \)).
Function.Bijective.comp theorem
{g : β → φ} {f : α → β} : Bijective g → Bijective f → Bijective (g ∘ f)
Full source 
theorem Bijective.comp {g : β → φ} {f : α → β} : Bijective g → Bijective f → Bijective (g ∘ f)
  | ⟨h_ginj, h_gsurj⟩, ⟨h_finj, h_fsurj⟩ => ⟨h_ginj.comp h_finj, h_gsurj.comp h_fsurj⟩
Composition of Bijective Functions is Bijective
Informal description
Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \phi$ be bijective functions. Then the composition $g \circ f \colon \alpha \to \phi$ is also bijective.
Function.LeftInverse definition
(g : β → α) (f : α → β) : Prop
Full source 
/-- `LeftInverse g f` means that `g` is a left inverse to `f`. That is, `g ∘ f = id`. -/
def LeftInverse (g : β → α) (f : α → β) : Prop :=
  ∀ x, g (f x) = x
Left inverse of a function
Informal description
Given two functions $g : \beta \to \alpha$ and $f : \alpha \to \beta$, the relation $\text{LeftInverse}\ g\ f$ holds if $g$ is a left inverse of $f$, meaning that for every $x \in \alpha$, we have $g(f(x)) = x$.
Function.HasLeftInverse definition
(f : α → β) : Prop
Full source 
/-- `HasLeftInverse f` means that `f` has an unspecified left inverse. -/
def HasLeftInverse (f : α → β) : Prop :=
  ∃ finv : β → α, LeftInverse finv f
Existence of a left inverse for a function
Informal description
A function \( f : \alpha \to \beta \) has a left inverse if there exists a function \( \text{finv} : \beta \to \alpha \) such that \( \text{finv} \circ f \) is the identity function on \( \alpha \), i.e., \( \text{finv}(f(x)) = x \) for all \( x \in \alpha \).
Function.RightInverse definition
(g : β → α) (f : α → β) : Prop
Full source 
/-- `RightInverse g f` means that `g` is a right inverse to `f`. That is, `f ∘ g = id`. -/
def RightInverse (g : β → α) (f : α → β) : Prop :=
  LeftInverse f g
Right inverse of a function
Informal description
Given two functions $g : \beta \to \alpha$ and $f : \alpha \to \beta$, the relation $\text{RightInverse}\ g\ f$ holds if $g$ is a right inverse of $f$, meaning that for every $y \in \beta$, we have $f(g(y)) = y$. In other words, the composition $f \circ g$ equals the identity function on $\beta$.
Function.HasRightInverse definition
(f : α → β) : Prop
Full source 
/-- `HasRightInverse f` means that `f` has an unspecified right inverse. -/
def HasRightInverse (f : α → β) : Prop :=
  ∃ finv : β → α, RightInverse finv f
Existence of a right inverse for a function
Informal description
A function \( f : \alpha \to \beta \) has a right inverse if there exists a function \( \text{finv} : \beta \to \alpha \) such that \( f \circ \text{finv} \) is the identity function on \( \beta \), i.e., \( f(\text{finv}(y)) = y \) for all \( y \in \beta \).
Function.LeftInverse.injective theorem
{g : β → α} {f : α → β} : LeftInverse g f → Injective f
Full source 
theorem LeftInverse.injective {g : β → α} {f : α → β} : LeftInverse g f → Injective f :=
  fun h a b faeqfb =>
  calc
    a = g (f a) := (h a).symm
    _ = g (f b) := congr_arg g faeqfb
    _ = b := h b
Left Inverse Implies Injective Function
Informal description
If a function $g : \beta \to \alpha$ is a left inverse of a function $f : \alpha \to \beta$ (i.e., $g \circ f = \text{id}$), then $f$ is injective.
Function.HasLeftInverse.injective theorem
{f : α → β} : HasLeftInverse f → Injective f
Full source 
theorem HasLeftInverse.injective {f : α → β} : HasLeftInverse f → Injective f := fun h =>
  Exists.elim h fun _finv inv => inv.injective
Existence of a Left Inverse Implies Injectivity
Informal description
If a function $f : \alpha \to \beta$ has a left inverse, then $f$ is injective.
Function.rightInverse_of_injective_of_leftInverse theorem
{f : α → β} {g : β → α} (injf : Injective f) (lfg : LeftInverse f g) : RightInverse f g
Full source 
theorem rightInverse_of_injective_of_leftInverse {f : α → β} {g : β → α} (injf : Injective f)
    (lfg : LeftInverse f g) : RightInverse f g := fun x =>
  have h : f (g (f x)) = f x := lfg (f x)
  injf h
Injective Function with Left Inverse has Right Inverse
Informal description
Let $f : \alpha \to \beta$ be an injective function and $g : \beta \to \alpha$ be a left inverse of $f$ (i.e., $g \circ f = \text{id}_\alpha$). Then $f$ is also a right inverse of $g$ (i.e., $f \circ g = \text{id}_\beta$).
Function.RightInverse.surjective theorem
{f : α → β} {g : β → α} (h : RightInverse g f) : Surjective f
Full source 
theorem RightInverse.surjective {f : α → β} {g : β → α} (h : RightInverse g f) : Surjective f :=
  fun y => ⟨g y, h y⟩
Right inverse implies surjectivity
Informal description
If a function $g : \beta \to \alpha$ is a right inverse of a function $f : \alpha \to \beta$ (i.e., $f \circ g = \text{id}_\beta$), then $f$ is surjective.
Function.HasRightInverse.surjective theorem
{f : α → β} : HasRightInverse f → Surjective f
Full source 
theorem HasRightInverse.surjective {f : α → β} : HasRightInverse f → Surjective f
  | ⟨_finv, inv⟩ => inv.surjective
Existence of Right Inverse Implies Surjectivity
Informal description
If a function $f : \alpha \to \beta$ has a right inverse, then $f$ is surjective.
Function.leftInverse_of_surjective_of_rightInverse theorem
{f : α → β} {g : β → α} (surjf : Surjective f) (rfg : RightInverse f g) : LeftInverse f g
Full source 
theorem leftInverse_of_surjective_of_rightInverse {f : α → β} {g : β → α} (surjf : Surjective f)
    (rfg : RightInverse f g) : LeftInverse f g := fun y =>
  Exists.elim (surjf y) fun x hx =>
    calc
      f (g y) = f (g (f x)) := hx ▸ rfl
      _ = f x := Eq.symm (rfg x) ▸ rfl
      _ = y := hx
Surjective Right Inverse Implies Left Inverse
Informal description
Let $f : \alpha \to \beta$ be a surjective function and $g : \beta \to \alpha$ be a right inverse of $f$ (i.e., $f \circ g = \text{id}_\beta$). Then $f$ is also a left inverse of $g$ (i.e., $g \circ f = \text{id}_\alpha$).
Function.injective_id theorem
: Injective (@id α)
Full source 
theorem injective_id : Injective (@id α) := fun _a₁ _a₂ h => h
Injectivity of the Identity Function
Informal description
The identity function $\mathrm{id} : \alpha \to \alpha$ is injective.
Function.surjective_id theorem
: Surjective (@id α)
Full source 
theorem surjective_id : Surjective (@id α) := fun a => ⟨a, rfl⟩
Surjectivity of the Identity Function
Informal description
The identity function $\mathrm{id} : \alpha \to \alpha$ is surjective, meaning that for every $y \in \alpha$, there exists an $x \in \alpha$ such that $\mathrm{id}(x) = y$.
Function.bijective_id theorem
: Bijective (@id α)
Full source 
theorem bijective_id : Bijective (@id α) :=
  ⟨injective_id, surjective_id⟩
Bijectivity of the Identity Function
Informal description
The identity function $\mathrm{id} : \alpha \to \alpha$ is bijective, meaning it is both injective and surjective.
Function.Injective.beq_eq theorem
{α β : Type*} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {f : α → β} (I : Injective f) {a b : α} : (f a == f b) = (a == b)
Full source 
theorem Injective.beq_eq {α β : Type*} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {f : α → β}
    (I : Injective f) {a b : α} : (f a == f b) = (a == b) := by
  by_cases h : a == b <;> simp [h] <;> simpa [I.eq_iff] using h
Injective Function Preserves Boolean Equality
Informal description
Let $\alpha$ and $\beta$ be types equipped with boolean equality operations `[BEq α]` and `[BEq β]` that satisfy the lawful equality axioms `[LawfulBEq α]` and `[LawfulBEq β]`. For any injective function $f : \alpha \to \beta$ and any elements $a, b \in \alpha$, the boolean equality comparison of $f(a)$ and $f(b)$ is equal to the boolean equality comparison of $a$ and $b$, i.e., $(f(a) == f(b)) = (a == b)$.
Function.Injective.ne theorem
(hf : Injective f) {a₁ a₂ : α} : a₁ ≠ a₂ → f a₁ ≠ f a₂
Full source 
theorem Injective.ne (hf : Injective f) {a₁ a₂ : α} : a₁ ≠ a₂ → f a₁ ≠ f a₂ :=
  mt fun h ↦ hf h
Injective Functions Preserve Inequality
Informal description
For any injective function $f : \alpha \to \beta$ and any elements $a_1, a_2 \in \alpha$, if $a_1 \neq a_2$, then $f(a_1) \neq f(a_2)$.
Function.Injective.ne_iff theorem
(hf : Injective f) {x y : α} : f x ≠ f y ↔ x ≠ y
Full source 
theorem Injective.ne_iff (hf : Injective f) {x y : α} : f x ≠ f yf x ≠ f y ↔ x ≠ y :=
  ⟨mt <| congr_arg f, hf.ne⟩
Inequality Preservation by Injective Functions
Informal description
For any injective function $f : \alpha \to \beta$ and any elements $x, y \in \alpha$, the inequality $f(x) \neq f(y)$ holds if and only if $x \neq y$.
Function.Injective.ne_iff' theorem
(hf : Injective f) {x y : α} {z : β} (h : f y = z) : f x ≠ z ↔ x ≠ y
Full source 
theorem Injective.ne_iff' (hf : Injective f) {x y : α} {z : β} (h : f y = z) : f x ≠ zf x ≠ z ↔ x ≠ y :=
  h ▸ hf.ne_iff
Inequality Preservation by Injective Functions (Parameterized Version)
Informal description
For any injective function $f \colon \alpha \to \beta$, elements $x, y \in \alpha$, and $z \in \beta$ such that $f(y) = z$, the inequality $f(x) \neq z$ holds if and only if $x \neq y$.
Function.LeftInverse.id theorem
{g : β → α} {f : α → β} (h : LeftInverse g f) : g ∘ f = id
Full source 
protected theorem LeftInverse.id {g : β → α} {f : α → β} (h : LeftInverse g f) : g ∘ f = id :=
  funext h
Composition of Left Inverse with Original Function Yields Identity
Informal description
If $g : \beta \to \alpha$ is a left inverse of $f : \alpha \to \beta$, then the composition $g \circ f$ is equal to the identity function on $\alpha$.
Function.RightInverse.id theorem
{g : β → α} {f : α → β} (h : RightInverse g f) : f ∘ g = id
Full source 
protected theorem RightInverse.id {g : β → α} {f : α → β} (h : RightInverse g f) : f ∘ g = id :=
  funext h
Composition of Right Inverse with Original Function Yields Identity
Informal description
If $g \colon \beta \to \alpha$ is a right inverse of $f \colon \alpha \to \beta$, then the composition $f \circ g$ equals the identity function on $\beta$.
Function.IsFixedPt definition
(f : α → α) (x : α)
Full source 
/-- A point `x` is a fixed point of `f : α → α` if `f x = x`. -/
def IsFixedPt (f : α → α) (x : α) := f x = x
Fixed point of a function
Informal description
A point \( x \) in a type \( \alpha \) is called a fixed point of a function \( f : \alpha \to \alpha \) if \( f(x) = x \).
Pi.map definition
(f : ∀ i, α i → β i) : (∀ i, α i) → (∀ i, β i)
Full source 
/-- Sends a dependent function `a : ∀ i, α i` to a dependent function `Pi.map f a : ∀ i, β i`
by applying `f i` to `i`-th component. -/
protected def map (f : ∀ i, α i → β i) : (∀ i, α i) → (∀ i, β i) := fun a i ↦ f i (a i)
Component-wise application of a family of functions
Informal description
Given a family of functions \( f_i : \alpha_i \to \beta_i \) indexed by \( i \in \iota \), the function \( \text{Pi.map} \) transforms a dependent function \( a : \forall i, \alpha_i \) into a new dependent function \( \text{Pi.map} \, f \, a : \forall i, \beta_i \) by applying \( f_i \) to the \( i \)-th component \( a_i \). More precisely, for each \( i \in \iota \), we have \( (\text{Pi.map} \, f \, a)_i = f_i (a_i) \).
Pi.map_apply theorem
(f : ∀ i, α i → β i) (a : ∀ i, α i) (i : ι) : Pi.map f a i = f i (a i)
Full source 
@[simp]
lemma map_apply (f : ∀ i, α i → β i) (a : ∀ i, α i) (i : ι) : Pi.map f a i = f i (a i) := rfl
Component-wise Evaluation of Pi.map
Informal description
For a family of functions $f_i : \alpha_i \to \beta_i$ indexed by $i \in \iota$, and a dependent function $a : \forall i, \alpha_i$, the $i$-th component of the mapped function $\text{Pi.map}\,f\,a$ is equal to $f_i$ applied to the $i$-th component of $a$, i.e., $(\text{Pi.map}\,f\,a)_i = f_i(a_i)$.