Function.id_comp
theorem Function.id_comp : ∀ {α : Sort u₁} {β : Sort u₂} (f : α → β), id ∘ f = f
This theorem, named `Function.id_comp`, states that for all functions `f` from some sort `α` to another sort `β`, the composition of the identity function `id` and `f` is equal to `f` itself. In other words, if you first apply `f` and then apply the identity function, it's the same as just applying `f`. This is a formalization of one of the basic properties of the identity function in function composition, as usually expressed in mathematics by \(id \circ f = f\).
More concisely: The identity function's composition with any function `f` is equal to `f`. In mathematical notation: `id ∘ f = f`.
|
Function.comp.right_id
theorem Function.comp.right_id : ∀ {α : Sort u₁} {β : Sort u₂} (f : α → β), f ∘ id = f
This theorem, referred to as `Function.comp.right_id`, states that for any function `f` from a type `α` to a type `β`, the composition of `f` with the identity function is equivalent to `f`. In other words, applying the identity function to the output of `f` does not change the function itself. This is an alias for the `Function.comp_id` theorem.
More concisely: For any function `f` from type `α` to type `β`, `f ∘ id = f`, where `id` is the identity function on `α`.
|
Function.Surjective.comp
theorem Function.Surjective.comp :
∀ {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : β → φ} {f : α → β},
Function.Surjective g → Function.Surjective f → Function.Surjective (g ∘ f)
The theorem `Function.Surjective.comp` states that for any three sorts (types) `α`, `β`, and `φ`, and any two functions `f` from `α` to `β` and `g` from `β` to `φ`, if `g` is surjective and `f` is surjective then their composition `g ∘ f` (first applying `f`, then `g`) is also surjective. In other words, if every element of `β` is the image of some element of `α` under `f`, and every element of `φ` is the image of some element of `β` under `g`, then every element of `φ` is the image of some element of `α` under the composition `g ∘ f`.
More concisely: If `f: α → β` and `g: β → φ` are functions with `g` surjective and `f` surjective, then their composition `g ∘ f` is also surjective.
|
Function.comp_const_right
theorem Function.comp_const_right :
∀ {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β → φ) (b : β), f ∘ Function.const α b = Function.const α (f b)
This theorem, named `Function.comp_const_right`, asserts that for any types `α`, `β`, and `φ`, and for any function `f` from `β` to `φ` and any element `b` of type `β`, the composition of `f` with the constant function at `b` is identical to the constant function at `f(b)`. This states that applying `f` to the result of the constant function is the same as making `f(b)` the new constant value.
More concisely: For any functions $f:\beta \to \varphi$ and $c:\beta \to \alpha$ being a constant function with value $b$, we have $c \circ f = \text{const}(f(b))$.
|
Function.left_id
theorem Function.left_id : ∀ {α : Sort u₁} {β : Sort u₂} (f : α → β), id ∘ f = f
This theorem, referred to as `Function.left_id`, states that for all types `α` and `β`, and for any function `f` mapping `α` to `β`, the composition of the identity function `id` and `f` is equal to `f` itself. This is an alias of the `Function.id_comp` theorem and captures the basic property of the identity function, namely that applying `id` to the result of a function does not change the outcome. In mathematical terms, this could be written as `(id ∘ f)(x) = f(x)` for all `x` in `α`.
More concisely: For any function `f` from type `α` to type `β`, the identity function's composition with `f` equals `f` itself: `id ∘ f = f`.
|
Function.right_id
theorem Function.right_id : ∀ {α : Sort u₁} {β : Sort u₂} (f : α → β), f ∘ id = f
The theorem `Function.right_id` is an alias of `Function.comp_id` and it states that for all types `α` and `β`, and for any function `f` from `α` to `β`, the composition of `f` with the identity function (`id`) is just `f`. This means applying the identity function to the output of `f` does not change the function `f` itself. In terms of mathematical notation, this is equivalent to stating that for any function `f: α → β`, we have `f ∘ id = f`, where `∘` denotes function composition and `id` is the identity function.
More concisely: The theorem `Function.right_id` asserts that for any function `f: α → β`, the composition of `f` with the identity function `id` over type `α` equals `f` itself. (i.e., `f ∘ id = f`)
|
Function.RightInverse.surjective
theorem Function.RightInverse.surjective :
∀ {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α}, Function.RightInverse g f → Function.Surjective f
The theorem `Function.RightInverse.surjective` states that for any two types `α` and `β`, and any two functions `f : α → β` and `g : β → α`, if `g` is a right inverse to `f` (i.e., the composition `f ∘ g` equals the identity function), then `f` is surjective. In other words, for every element `b` in `β`, there exists an element `a` in `α` such that `f(a) = b`.
More concisely: If `f : α → β` has a right inverse `g : β → α` in Lean 4, then `f` is surjective.
|
Function.HasLeftInverse.injective
theorem Function.HasLeftInverse.injective :
∀ {α : Sort u₁} {β : Sort u₂} {f : α → β}, Function.HasLeftInverse f → Function.Injective f
This theorem states that for any given function `f` mapping from a type `α` to another type `β`, if `f` has a left inverse (there exists a function that, when composed with `f` from the left, yields the identity function on `α`), then `f` is injective. In the language of mathematics, this means that if `f : α → β` has a function `g : β → α` such that `g ∘ f = id_α`, then `f` is injective (for any `x, y ∈ α`, if `f(x) = f(y)`, then `x = y`).
More concisely: If a function `f : α → β` has a left inverse, then it is injective (i.e., for all `x, y ∈ α`, if `f(x) = f(y)` then `x = y`).
|
Function.Injective.comp
theorem Function.Injective.comp :
∀ {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : β → φ} {f : α → β},
Function.Injective g → Function.Injective f → Function.Injective (g ∘ f)
The theorem `Function.Injective.comp` states that given any three types `α`, `β`, and `φ`, and any two functions `g : β → φ` and `f : α → β`, if `g` and `f` are both injective (i.e., for any two inputs that are equal after applying the function, the inputs must have been equal), then the composition of `g` and `f` (denoted `g ∘ f`), where `f` is applied first and then `g` is applied to the result, is also injective. In other words, the injective property is preserved under function composition.
More concisely: If functions `f : α → β` and `g : β → φ` are both injective, then their composition `g ∘ f : α → φ` is also injective.
|
Function.comp.assoc
theorem Function.comp.assoc :
∀ {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} (f : φ → δ) (g : β → φ) (h : α → β),
(f ∘ g) ∘ h = f ∘ g ∘ h
This theorem states that for any four types `α`, `β`, `φ`, and `δ`, and for any three functions `f` from `φ` to `δ`, `g` from `β` to `φ`, and `h` from `α` to `β`, the composition of functions is associative. That is, composing `f` with `g` and then composing the result with `h` (`(f ∘ g) ∘ h`) is the same as composing `f` with the composition of `g` and `h` (`f ∘ (g ∘ h)`). This means that we can change the grouping of the composition without changing the overall result.
More concisely: For any types `α`, `β`, `φ`, and functions `f : φ -> δ`, `g : β -> φ`, and `h : α -> β`, the associativity of function composition holds: `(f ∘ g) ∘ h = f ∘ (g ∘ h)`.
|
Function.bijective_id
theorem Function.bijective_id : ∀ {α : Sort u₁}, Function.Bijective id
The theorem `Function.bijective_id` states that for all types `α`, the identity function `id` is bijective. In mathematical terms, this means that the identity function, which maps each element of a type to itself, is both injective (no two different elements map to the same element) and surjective (every element of the type is the image of at least one element), thus forming a one-to-one correspondence between the elements of the type.
More concisely: The identity function is a bijection on any type.
|
Function.comp.left_id
theorem Function.comp.left_id : ∀ {α : Sort u₁} {β : Sort u₂} (f : α → β), id ∘ f = f
This theorem, named `Function.comp.left_id`, states that for any types `α` and `β` and any function `f` from `α` to `β`, the composition of the identity function (denoted as `id`) and `f` is equal to `f` itself. In other words, applying `id` to the result of `f` has no effect, so `id ∘ f` is indeed just `f`. This is an alias of the `Function.id_comp` theorem.
More concisely: The theorem asserts that for all types `α` and `β` and functions `f` from `α` to `β`, the identity function's composition with `f` equals `f` itself (`id ∘ f = f`).
|
Function.surjective_id
theorem Function.surjective_id : ∀ {α : Sort u₁}, Function.Surjective id
This theorem states that for any type `α`, the identity function is surjective. In other words, for any `α`, each element of `α` is mapped to by some element of `α` under the identity function. In mathematical terms, this means that for every `b` in `α`, there exists an `a` in `α` such that `id a = b`, which always holds true as `id a` is always `a`.
More concisely: For any type `α`, the identity function `id : α → α` is surjective.
|
Function.leftInverse_of_surjective_of_rightInverse
theorem Function.leftInverse_of_surjective_of_rightInverse :
∀ {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α},
Function.Surjective f → Function.RightInverse f g → Function.LeftInverse f g
This theorem states that for any two functions `f : α → β` and `g : β → α`, if `f` is surjective (that is, for every element `b` in `β` there exists an element `a` in `α` such that `f(a) = b`) and `g` is a right inverse to `f` (i.e., `f ∘ g = id`), then `g` is also a left inverse to `f` (meaning `g ∘ f = id`). In other words, if every element in the codomain is mapped from the domain by `f` and applying `f` after `g` gives you the same value, then applying `g` after `f` will also give you the original value.
More concisely: If `f : α → β` is surjective and has a right inverse `g : β → α`, then `g` is a left inverse of `f`. That is, `f ∘ g = id_β` and `g ∘ f = id_α`.
|
Function.rightInverse_of_injective_of_leftInverse
theorem Function.rightInverse_of_injective_of_leftInverse :
∀ {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α},
Function.Injective f → Function.LeftInverse f g → Function.RightInverse f g
The theorem `Function.rightInverse_of_injective_of_leftInverse` states that for all types `α` and `β`, and for all functions `f` from `α` to `β` and `g` from `β` to `α`, if `f` is injective and `f` is a left inverse to `g`, then `f` is also a right inverse to `g`. In other words, if every element in the codomain `β` is mapped by `f` from a unique element in the domain `α` (injectivity), and applying `f` after `g` gives the identity function on `β` (left inverseness), then applying `g` after `f` gives the identity function on `α` (right inverseness).
More concisely: If `f: α → β` is injective and left-inverse to `g: β → α`, then `g` is right-inverse to `f`. In other words, `f ∘ g = idβ` and `g ∘ f = idα`.
|
Function.Bijective.comp
theorem Function.Bijective.comp :
∀ {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : β → φ} {f : α → β},
Function.Bijective g → Function.Bijective f → Function.Bijective (g ∘ f)
The theorem `Function.Bijective.comp` states that for any three types `α`, `β`, and `φ`, and any two functions `f : α → β` and `g : β → φ`, if `g` is bijective (both injective and surjective) and `f` is also bijective, then the composition of `g` and `f` (denoted as `g ∘ f`) is also bijective. In other words, the composition of two bijective functions is always a bijective function.
More concisely: If functions `f : α → β` and `g : β → φ` are both bijective, then their composition `g ∘ f` is also bijective.
|
Function.LeftInverse.injective
theorem Function.LeftInverse.injective :
∀ {α : Sort u₁} {β : Sort u₂} {g : β → α} {f : α → β}, Function.LeftInverse g f → Function.Injective f
The theorem `Function.LeftInverse.injective` states that for all types `α` and `β`, and for all functions `g : β → α` and `f : α → β`, if `g` is a left inverse to `f` (meaning that for every `x : α`, applying `f` and then `g` gives back `x`), then `f` is injective. An injective function is one where if `f x = f y` then `x` must equal `y`, or in other words, no two different inputs give the same output.
More concisely: If a function `g : β → α` is a left inverse of `f : α → β`, then `f` is injective. That is, for all `x, y : α`, if `f x = f y` then `x = y`.
|
Function.uncurry_curry
theorem Function.uncurry_curry :
∀ {α : Type u₁} {β : Type u₂} {φ : Type u₃} (f : α × β → φ), Function.uncurry (Function.curry f) = f
The theorem `Function.uncurry_curry` states that for all types `α`, `β`, and `φ`, and for any function `f` which takes a pair of elements (one from `α` and one from `β`) and returns an element of `φ`, if we first curry this function `f` (transform it into a function that takes two arguments separately) and then uncurry it (transform it back into a function that takes a pair of arguments), we get the original function `f`. This theorem thus asserts the consistency of the curry and uncurry operations; currying followed by uncurrying a function always brings us back to the original function.
More concisely: For any function `f : α × β → φ`, the functions `(λ x y => f (x, y))` and `λ p => f p.fst p.snd` are equal. (Here, `α × β` denotes the Cartesian product of types `α` and `β`, `p` is a pair, `p.fst` is the first component of the pair, and `p.snd` is the second component of the pair.)
|
Function.injective_id
theorem Function.injective_id : ∀ {α : Sort u₁}, Function.Injective id
The theorem `Function.injective_id` states that, for every type `α` in some universe `u₁`, the identity function on that type (denoted by `id` in Lean 4) is injective. This means that if `id x = id y` for any two elements `x` and `y` of `α`, it must be the case that `x = y`. In other words, the identity function on any type does not map distinct elements to the same element.
More concisely: For any type `α`, the identity function `id` is a injective function, that is, for all `x` and `y` in `α`, `id x = id y` implies `x = y`.
|
Function.comp_id
theorem Function.comp_id : ∀ {α : Sort u₁} {β : Sort u₂} (f : α → β), f ∘ id = f
This theorem, called `Function.comp_id`, states that for all types `α` and `β`, and for any function `f` from `α` to `β`, the composition of `f` with the identity function is equal to `f` itself. In mathematical notation, if `f : α → β`, then `f ∘ id = f`. This is a restatement of the identity law for functions.
More concisely: For all types `α` and functions `f : α → β`, the composition of `f` with the identity function is equal to `f`: `f ∘ id = f`.
|