Function.Bijective.existsUnique
theorem Function.Bijective.existsUnique :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Bijective f → ∀ (b : β), ∃! a, f a = b
This theorem states that for any types `α` and `β`, and any function `f` from `α` to `β`, if `f` is bijective (meaning it is both injective and surjective), then for any element `b` of `β`, there exists a unique element `a` in `α` such that `f(a) = b`. In other words, every element in the codomain `β` corresponds to exactly one element in the domain `α`, which is a characteristic property of bijective functions.
More concisely: For any bijective function `f` from type `α` to type `β`, for all `b` in `β`, there exists a unique `a` in `α` such that `f(a) = b`.
|
Symmetric.forall_existsUnique_iff
theorem Symmetric.forall_existsUnique_iff :
∀ {α : Sort u_1} {r : α → α → Prop},
Symmetric r → ((∀ (a : α), ∃! b, r a b) ↔ ∃ f, Function.Involutive f ∧ ∀ {a b : α}, r a b ↔ f a = b)
The theorem states that for any symmetric relation `r` on a sort `α`, `r` behaves like a function (i.e., for each element `a` of type `α`, there exists a unique `b` such that `r a b`) if and only if `r` can be expressed as the equality relation `f a = b` for some function `f` that is involutive (i.e., `f(f(x)) = x` for all `x`).
More concisely: A symmetric relation on a sort behaves like a function if and only if it can be expressed as the equality relation of an involutive function.
|
Function.Injective.extend_apply
theorem Function.Injective.extend_apply :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
Function.Injective f → ∀ (g : α → γ) (e' : β → γ) (a : α), Function.extend f g e' (f a) = g a
The theorem `Function.Injective.extend_apply` states that for any types `α`, `β`, and `γ`, and any function `f` from `α` to `β`, if `f` is injective, then for any function `g` from `α` to `γ`, any function `e'` from `β` to `γ`, and any element `a` of `α`, applying the extension of `f` by `g` and `e'` to `f(a)` yields `g(a)`. In other words, when we extend an injective function with another function, the value of the extended function at any point is the same as the value of the original function at that point.
More concisely: If `f: α → β` is injective and `g: α → γ` and `e': β → γ` are functions, then for all `a ∈ α`, `(extend f g e') a = g a`.
|
Function.Injective2.left'
theorem Function.Injective2.left' :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ},
Function.Injective2 f → ∀ [inst : Nonempty β], Function.Injective f
This theorem, `Function.Injective2.left'`, states that if a binary function `f : α → β → γ` is injective in both its arguments, as defined by `Function.Injective2`, then considering `f` as a map from its left argument to a unary function (that is, considering `f` as a function `f : α → (β → γ)`), `f` is also injective, as defined by `Function.Injective`. This conclusion depends on the fact that the second input space `β` is nonempty, represented in Lean by the `Nonempty β` typeclass instance.
More concisely: If a binary function `f : α → β → γ` is injective in both arguments, then the function `f` considered as a map from `α` to `(β → γ)` is also injective. This holds when the domain of the second argument `β` is nonempty.
|
Function.Surjective.exists
theorem Function.Surjective.exists :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Surjective f → ∀ {p : β → Prop}, (∃ y, p y) ↔ ∃ x, p (f x)
The theorem `Function.Surjective.exists` states that for all types `α` and `β`, and any function `f` from `α` to `β`, if `f` is surjective, then for any predicate `p` over `β`, there exists an element `y` in `β` such that `p` holds for `y` if and only if there exists an element `x` in `α` such that `p` holds for `f(x)`. In other words, it says that if a condition holds for some element in the range of a surjective function, then it must hold for some element in the domain when applied to the function.
More concisely: If `f` is a surjective function from type `α` to type `β`, then for any predicate `p` over `β`, there exists an `x` in `α` such that `p(f(x))` holds if and only if there exists a `y` in `β` such that `p(y)` holds.
|
Function.FactorsThrough.extend_apply
theorem Function.FactorsThrough.extend_apply :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : α → γ},
Function.FactorsThrough g f → ∀ (e' : β → γ) (a : α), Function.extend f g e' (f a) = g a
The theorem `Function.FactorsThrough.extend_apply` states that for any types `α`, `β`, and `γ`, and any functions `f : α → β`, `g : α → γ`, if `g` factors through `f` (i.e., if `f a = f b` implies that `g a = g b` for any `a` and `b` in `α`), then for every function `e' : β → γ` and every element `a` of `α`, the function `Function.extend f g e'` evaluated at `f a` is equal to `g a`. This theorem effectively asserts that the extension of `g` via `f` and `e'` maintains the original behavior of `g` when evaluated at `f a`.
More concisely: If `f` and `g` are functions with `g` factoring through `f`, then `Function.extend f g e' (f a)` equals `g a` for all `e' : β → γ` and `a : α`.
|
forall_existsUnique_iff
theorem forall_existsUnique_iff :
∀ {α : Sort u_1} {β : Sort u_2} {r : α → β → Prop},
(∀ (a : α), ∃! b, r a b) ↔ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b
The theorem `forall_existsUnique_iff` states that for any relation `r` mapping from type `α` to `β`, the relation is function-like (meaning for every `a` of type `α`, there exists a unique `b` of type `β` such that relation `r` holds on `a` and `b`) if and only if there exists a function `f` such that for any `a` of type `α` and `b` of type `β`, the relation `r` holds on `a` and `b` if and only if `f(a)` equals `b`.
More concisely: For any relation between types `α` and `β`, it is function-like if and only if there exists a function from `α` to `β` that makes the relation equivalence between elements in `α` and their images under that function.
|
Function.RightInverse.comp_eq_id
theorem Function.RightInverse.comp_eq_id :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.RightInverse f g → g ∘ f = id
The theorem `Function.RightInverse.comp_eq_id` states that for any types `α` and `β`, and for any functions `f` from `α` to `β` and `g` from `β` to `α`, if `f` is a function such that `g` is a right inverse to `f` (that is, `f ∘ g = id`, where `id` is the identity function), then the composition of `g` with `f` is equal to the identity function. In other words, if you first apply `f` and then `g`, you end up where you started, which is what it means for `g` to be a right inverse of `f`.
More concisely: If `f: α → β` has a right inverse `g: β → α` (i.e., `f ∘ g = id`), then `g ∘ f = id`.
|
Function.forall_update_iff
theorem Function.forall_update_iff :
∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (f : (a : α) → β a) {a : α} {b : β a}
(p : (a : α) → β a → Prop), (∀ (x : α), p x (Function.update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
The theorem `Function.forall_update_iff` states that for every function `f` from a type `α` to another type `β`, a particular point `a` in `α`, a value `b` in `β a`, and a property `p` which takes a point in `α` and a value in `β a`, asserting that this property `p` holds for every point in the domain `α` after updating the function `f` at the point `a` with the value `b`, is equivalent to stating that this property `p` holds at the point `a` with the value `b` and at every other point `x` in the domain `α` with the original function value `f x`, given that `x` is not equal to `a`.
More concisely: For any function `f` from type `α` to type `β`, point `a` in `α`, value `b` in `β`, and property `p`, the function `f` updates `a` to `b` with property `p` if and only if `p` holds at `a` with `b` and for all `x ≠ a` in `α`, `p` holds at `x` with `f x`.
|
Function.update_apply
theorem Function.update_apply :
∀ {α : Sort u} [inst : DecidableEq α] {β : Sort u_1} (f : α → β) (a' : α) (b : β) (a : α),
Function.update f a' b a = if a = a' then b else f a
This theorem states that for non-dependent functions, the `Function.update` operation can be expressed as an "if-then-else" statement. More specifically, given any types `α` and `β`, a function `f` from `α` to `β`, elements `a'` of `α` and `b` of `β`, and a decidable equality on `α`, the result of updating the function `f` at the point `a'` with the value `b` and then applying the updated function at `a` is the same as: if `a` equals `a'`, then `b` is returned, else the original function `f` is applied at `a`.
More concisely: For decidable equalities on type `α`, the update operation `Function.update f a' {b}` equals the if-then-elses `if a = a' then b else f a`.
|
Function.not_surjective_Type
theorem Function.not_surjective_Type : ∀ {α : Type u} (f : α → Type (max u v)), ¬Function.Surjective f
This theorem asserts that no surjective function exists from a type `α` of universe `u` into the type universe `Type (max u v)`. In other words, there cannot be a function `f` from `α` to `Type (max u v)` such that every type in `Type (max u v)` is the image of some element of `α` under `f`. This demonstrates the inconsistency of `Type : Type` in Lean, as it would lead to paradoxes analogous to Russell's paradox in set theory.
More concisely: There does not exist a surjective function from any type `α` to the universe `Type (max u v)` in Lean.
|
Function.bijective_iff_existsUnique
theorem Function.bijective_iff_existsUnique :
∀ {α : Sort u_1} {β : Sort u_2} (f : α → β), Function.Bijective f ↔ ∀ (b : β), ∃! a, f a = b
The theorem `Function.bijective_iff_existsUnique` states that for all types `α` and `β` and for a function `f` from `α` to `β`, `f` is bijective if and only if for every element `b` in `β`, there exists a unique element `a` in `α` such that `f(a) = b`. In other words, a function is bijective (both injective and surjective) if each element of the codomain is mapped exactly by one element from the domain.
More concisely: A function from type `α` to type `β` is bijective if and only if for every `b` in `β`, there exists a unique `a` in `α` such that `f(a) = b`.
|
forall_existsUnique_iff'
theorem forall_existsUnique_iff' :
∀ {α : Sort u_1} {β : Sort u_2} {r : α → β → Prop}, (∀ (a : α), ∃! b, r a b) ↔ ∃ f, r = fun x x_1 => f x = x_1 := by
sorry
The theorem `forall_existsUnique_iff'` states that a relation `r` from a type `α` to another type `β` behaves like a function (i.e., for each value of type `α`, there exists a unique value of type `β` such that `r` relates the two) if and only if there exists a function `f` such that `r` can be represented as the equation `f x = x_1` for every `x` of type `α` and `x_1` of type `β`. This theorem is essentially a formalization of the property that a relation is function-like if it relates each element of its domain to a unique element in its codomain.
More concisely: A relation between types behaves like a function if and only if there exists a function such that every element in the domain is related to exactly one element in the codomain through this function.
|
Function.update_eq_iff
theorem Function.update_eq_iff :
∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] {a : α} {b : β a} {f g : (a : α) → β a},
Function.update f a b = g ↔ b = g a ∧ ∀ (x : α), x ≠ a → f x = g x
The `Function.update_eq_iff` theorem states that for any types `α` and `β`, given `α` has decidable equality, for any elements `a` of type `α` and `b` of type `β a`, and for any two functions `f` and `g` from `α` to `β`, the function resulting from updating `f` at `a` with `b` is equal to `g` if and only if `b` is equal to the value of `g` at `a` and for every `x` in `α` not equal to `a`, the values of `f` and `g` at `x` are the same.
More concisely: For functions `f` and `g` from a decidably equated type `α` to type `βα`, `Function.update f a b = g a ∧ ∀ x ≠ a, f x = g x` if and only if `b = g a`.
|
Function.Involutive.comp_self
theorem Function.Involutive.comp_self : ∀ {α : Sort u} {f : α → α}, Function.Involutive f → f ∘ f = id
The theorem `Function.Involutive.comp_self` states that for any type `α` and any function `f` from `α` to `α`, if `f` is involutive (that is, applying `f` twice to any value `x` of type `α` results in `x` itself), then the composition of `f` with itself is the identity function. In terms of standard mathematical notation, if $f \circ f = Id$ for all `x` in `α`, then $f \circ f = Id$.
More concisely: If `α` is a type and `f : α → α` is an involutive function, then `f ∘ f = Id`.
|
Function.injective_surjInv
theorem Function.injective_surjInv :
∀ {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f), Function.Injective (Function.surjInv h) := by
sorry
The theorem `Function.injective_surjInv` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, if `f` is surjective (meaning that for every element `b` in `β`, there exists an element `a` in `α` such that `f(a) = b`), then the inverse function of `f`, denoted as `Function.surjInv h` where `h` is the surjectivity of `f`, is injective. An injective function is defined as a function where if `f(x) = f(y)`, then `x` must be equal to `y`. In other words, different inputs will always produce different outputs in an injective function.
More concisely: If a function is surjective, then its inverse is injective.
|
Function.Injective.ne
theorem Function.Injective.ne :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Injective f → ∀ {a₁ a₂ : α}, a₁ ≠ a₂ → f a₁ ≠ f a₂
This theorem states that for any types `α` and `β` and any function `f : α → β`, if the function `f` is injective (which means that for any two elements `a₁` and `a₂` in `α`, `f a₁ = f a₂` only if `a₁ = a₂`), then for any two different elements `a₁` and `a₂` in `α` (`a₁ ≠ a₂`), their images under `f` are also different (`f a₁ ≠ f a₂`). In other words, an injective function preserves distinctness.
More concisely: If `f : α → β` is an injective function, then for all `a₁, a₂ ∈ α` with `a₁ ≠ a₂`, it follows that `f a₁ ≠ f a₂`.
|
Function.update_eq_self
theorem Function.update_eq_self :
∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (a : α) (f : (a : α) → β a), Function.update f a (f a) = f
This theorem, `Function.update_eq_self`, states that for any type `α` that has a decidable equality and a dependent type `β`, for any element `a` of type `α` and any function `f` from `α` to `β`, if we update the function `f` at the point `a` with its own value `f(a)`, we get the same function `f` back. In other words, replacing the value of a function at a certain point by the value that was already there doesn't change the function.
More concisely: For any type `α` with decidable equality and any function `f` from `α` to a type `β`, `Function.update f a (f a) = f`.
|
Function.injective_iff_hasLeftInverse
theorem Function.injective_iff_hasLeftInverse :
∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β}, Function.Injective f ↔ Function.HasLeftInverse f
This theorem states that for any types `α` and `β` with `α` being nonempty, and any function `f` from `α` to `β`, the function `f` is injective if and only if `f` has a left inverse. In mathematical terms, a function `f: α → β` is injective if each element in `β` is mapped to by at most one element in `α`, and `f` has a left inverse if there exists another function that when composed with `f` from the left, results in the identity function on `α`. The theorem establishes a correspondence between these two properties of a function.
More concisely: A function `f: α → β` with nonempty `α` is injective if and only if there exists a function `g: β → α` such that `f ∘ g = idα`.
|
Function.invFun_surjective
theorem Function.invFun_surjective :
∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β},
Function.Injective f → Function.Surjective (Function.invFun f)
This theorem states that for any types `α` and `β`, where `α` is nonempty, and any function `f` from `α` to `β`, if the function `f` is injective, then the inverse of `f` is surjective. In other words, if for a function `f`, the condition "for all pairs of elements in `α`, if `f` applied to the first element equals `f` applied to the second element, then the first and second elements are the same" holds true, then for the inverse of this function, for every element in the codomain `β`, there exists an element in the domain `α` such that the inverse function applied to the former equals the latter.
More concisely: If `α` is nonempty and `f` is a function from `α` to `β` that is injective, then the inverse function `g:` `β` `→` `α` is surjective.
|
Function.Surjective.comp_left
theorem Function.Surjective.comp_left :
∀ {α : Sort u} {β : Sort v} {γ : Sort w} {g : β → γ}, Function.Surjective g → Function.Surjective fun x => g ∘ x
The theorem "Function.Surjective.comp_left" states that the composition of a function with a surjective function on the left is also surjective. In other words, for any types α, β, and γ, and for any function `g` from β to γ, if `g` is surjective, then the composition of `g` with any function from α to β is also surjective. In mathematical terms, if there exists a `g` such that for every element `c` in the codomain there exists an element `b` in the domain that `g(b) = c`, then for any function `f` from α to β, there exists an `a` in domain α that `(g ∘ f)(a) = c`.
More concisely: If `g` is a surjective function from β to γ, then the composition `g ∘ f` is surjective for any function `f` from α to β.
|
Function.Surjective.of_comp_iff
theorem Function.Surjective.of_comp_iff :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α},
Function.Surjective g → (Function.Surjective (f ∘ g) ↔ Function.Surjective f)
This theorem states that for all types `α`, `β`, and `γ`, given a function `f` from `α` to `β` and a function `g` from `γ` to `α`, if `g` is surjective (i.e., for every element of `α` there exists an element of `γ` such that `g` of that element equals the element of `α`), then `f` composition `g` (denoted by `f ∘ g`) is surjective if and only if `f` is surjective. In mathematical terms, this would mean that for all `b` in `β`, there exists an `a` in `α` such that `f(a) = b` if and only if for all `b` in `β`, there exists a `c` in `γ` such that `(f ∘ g)(c) = b`.
More concisely: For functions `f: α -> β` and `g: γ -> α`, if `g` is surjective and `f` is surjective then `f ∘ g` is surjective.
|
Function.update_comp_eq_of_forall_ne
theorem Function.update_comp_eq_of_forall_ne :
∀ {α' : Sort w} [inst : DecidableEq α'] {α : Sort u_1} {β : Sort u_2} (g : α' → β) {f : α → α'} {i : α'} (a : β),
(∀ (x : α), f x ≠ i) → Function.update g i a ∘ f = g ∘ f
The theorem `Function.update_comp_eq_of_forall_ne` states that for any types `α'`, `α`, and `β`, given a function `g` from `α'` to `β`, a function `f` from `α` to `α'`, an element `i` of `α'`, and an element `a` of `β`, if for all `x` in `α`, `f(x)` is not equal to `i`, then updating the function `g` at `i` with `a` and then composing with `f` is the same as just composing `g` with `f`. In other words, if `f` never outputs `i`, then updating `g` at `i` doesn't affect the composition of `g` with `f`.
More concisely: For functions `g : α' → β` and `f : α → α'`, if `i ≠ f(x)` for all `x ∈ α`, then `(g ∘ f)(x) = g(i • f(x))` for all `x ∈ α`, where `•` denotes function application.
|
Function.apply_update
theorem Function.apply_update :
∀ {ι : Sort u_1} [inst : DecidableEq ι] {α : ι → Sort u_2} {β : ι → Sort u_3} (f : (i : ι) → α i → β i)
(g : (i : ι) → α i) (i : ι) (v : α i) (j : ι),
f j (Function.update g i v j) = Function.update (fun k => f k (g k)) i (f i v) j
The theorem `Function.apply_update` states that for any types `ι`, `α`, and `β`, where `α` and `β` are type functions indexed by `ι`, given a function `f` that maps an element of type `ι` and its corresponding `α` value to a `β` value, another function `g` that maps an element of `ι` to an `α` value, an element `i` of type `ι`, a value `v` of type `α i`, and another element `j` of type `ι`, applying `f` to `j` and the result of updating `g` at `i` with `v`, is equivalent to updating the function that maps `k` to `f k (g k)` at `i` with `f i v`, and then applying this to `j`. This theorem essentially describes how function application interacts with function update.
More concisely: For any functions `f : ι → α → β` and `g : ι → α`, given `i : ι`, `v : α i`, and `j : ι`, `f i (g ^^ update i v) = update i (f i v) (g) ^^ f j`.
|
Function.update_comp_eq_of_injective
theorem Function.update_comp_eq_of_injective :
∀ {α : Sort u} {α' : Sort w} [inst : DecidableEq α] [inst_1 : DecidableEq α'] {β : Sort u_1} (g : α' → β)
{f : α → α'},
Function.Injective f → ∀ (i : α) (a : β), Function.update g (f i) a ∘ f = Function.update (g ∘ f) i a
This theorem, named `Function.update_comp_eq_of_injective`, states the following: For any types `α`, `α'`, and `β`, given that `α` and `α'` have decidable equality, and given a function `g` from `α'` to `β`, and an injective function `f` from `α` to `α'`, for any element `i` of `α` and `a` of `β`, the composition of the function `g` updated at `(f i)` with the value `a` and the function `f` is equal to the function `g ∘ f` updated at `i` with the value `a`.
In other words, if we have an injective function `f` and another function `g`, then updating `g` at `f(i)` and then applying `f` is the same as first applying `f` and then updating `g ∘ f` at `i`. This is a property about function composition and updating a function's value at a particular point.
More concisely: For injective functions `f: α → α'` and `g: α' → β`, the function update `(g : α' → β) ((f x) : α')` is equal to the composition `(g ∘ f) x` for all `x: α`. (Assuming `α`, `α'`, and `β` have decidable equality.)
|
Function.Involutive.injective
theorem Function.Involutive.injective : ∀ {α : Sort u} {f : α → α}, Function.Involutive f → Function.Injective f := by
sorry
The theorem states that for any type `α` and any function `f` from `α` to `α`, if `f` is involutive (meaning applying `f` twice to any element yields the original element), then `f` is also injective (meaning that no two different elements of `α` are mapped to the same element by `f`). In mathematical terms, if for a function `f : α → α`, we have `f(f(x)) = x` for all `x` in `α`, this theorem guarantees that if `f(x) = f(y)` for some `x` and `y` in `α`, then necessarily `x = y`.
More concisely: If a function from a type to itself is involutive (i.e., applying it twice to any element equals the original element), then it is injective (i.e., no two distinct elements are mapped to the same image).
|
Function.Bijective.of_comp_iff'
theorem Function.Bijective.of_comp_iff' :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
Function.Bijective f → ∀ (g : γ → α), Function.Bijective (f ∘ g) ↔ Function.Bijective g
This theorem states that for any types `α`, `β`, and `γ`, and for any function `f` from `α` to `β`, if `f` is bijective (both injective and surjective), then for any function `g` from `γ` to `α`, the composition `f ∘ g` is bijective if and only if `g` is bijective. In other words, when `f` is a bijective function, the bijectivity of the composition `f ∘ g` is equivalent to the bijectivity of `g` itself.
More concisely: If `f: α -> β` is a bijective function and `g: γ -> α` is any function, then `f ∘ g` is bijective if and only if `g` is bijective.
|
Function.LeftInverse.comp_eq_id
theorem Function.LeftInverse.comp_eq_id :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.LeftInverse f g → f ∘ g = id
The theorem `Function.LeftInverse.comp_eq_id` states that for all types `α` and `β`, and for all functions `f` from `α` to `β` and `g` from `β` to `α`, if `f` is a left inverse function to `g`, then the composition of `f` and `g` is the identity function. In mathematical terms, if for all `x` in `α`, `f(g(x)) = x`, then `f(g) = id`.
More concisely: If function `f` is a left inverse of `g` (i.e., `f ∘ g = id_α`), then `g ∘ f = id_β`.
|
Function.invFun_eq
theorem Function.invFun_eq :
∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β} {b : β},
(∃ a, f a = b) → f (Function.invFun f b) = b
This theorem states that for any types `α` and `β` where `α` is nonempty, given a function `f` from `α` to `β` and an element `b` of `β`, if there exists an element `a` of `α` such that `f(a)` equals `b`, then applying `f` to the inverse of `b` under the function `f` will yield `b` back. In other words, if `b` is in the image of `f`, then the function `f` composed with its inverse function at `b` equals `b`, which is a property demonstrating how the inverse function undoes the mapping of `f`.
More concisely: If `f` is a function from a nonempty type `α` to `β`, `b` is an element of `β` in the image of `f`, then `f(f⁻¹(b)) = b`.
|
Function.bijective_iff_has_inverse
theorem Function.bijective_iff_has_inverse :
∀ {α : Sort u} {β : Sort v} {f : α → β},
Function.Bijective f ↔ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f
This theorem states that for all types `α` and `β` and a function `f` from `α` to `β`, the function `f` is bijective if and only if there exists a function `g` such that `g` is a left inverse and a right inverse to `f`. In mathematical terms, a function is bijective - meaning it is both injective (or one-to-one) and surjective (or onto) - if and only if it has an inverse function that, when composed with the original function from both sides (left and right), yields the identity function.
More concisely: A function `f` from type `α` to type `β` is bijective if and only if there exists a function `g` such that `f ∘ g = idα` and `g ∘ f = idβ`, where `idα` and `idβ` are the identity functions on types `α` and `β`, respectively.
|
Function.Injective2.uncurry
theorem Function.Injective2.uncurry :
∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {f : α → β → γ},
Function.Injective2 f → Function.Injective (Function.uncurry f)
This theorem asserts that for any given types `α`, `β`, and `γ`, and any binary function `f : α → β → γ`, if `f` is injective in two variables (meaning that if `f` applied to `(a₁, b₁)` equals `f` applied to `(a₂, b₂)`, then `a₁` equals `a₂` and `b₁` equals `b₂`), then the uncurried version of `f` (which is a function `α × β → γ`) is also injective (meaning that if `f` applied to a pair `(a₁, b₁)` equals `f` applied to another pair `(a₂, b₂)`, then the two pairs `(a₁, b₁)` and `(a₂, b₂)` are equal).
More concisely: If a binary function `f : α → β → γ` is injective in both variables, then its uncurried version `f : α × β → γ` is also injective.
|
Function.Surjective.of_comp_iff'
theorem Function.Surjective.of_comp_iff' :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
Function.Bijective f → ∀ (g : γ → α), Function.Surjective (f ∘ g) ↔ Function.Surjective g
This theorem states that for any types `α`, `β`, and `γ`, and for any function `f` from `α` to `β` that is bijective (both injective and surjective), for any function `g` from `γ` to `α`, the composition of `f` and `g` (denoted by `f ∘ g`) is surjective if and only if `g` itself is surjective. In other words, if every element of `β` can be obtained by applying `f ∘ g` to some element of `γ`, then every element of `α` can also be obtained by applying `g` to some element of `γ`.
More concisely: For any types `α`, `β`, and `γ`, if `f: α → β` is bijective and `g: γ → α`, then `f ∘ g` is surjective if and only if `g` is surjective.
|
Function.eq_update_iff
theorem Function.eq_update_iff :
∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] {a : α} {b : β a} {f g : (a : α) → β a},
g = Function.update f a b ↔ g a = b ∧ ∀ (x : α), x ≠ a → g x = f x
The theorem `Function.eq_update_iff` states that for any types `α` and `β` where `β` is a type dependent on `α`, given a decidable equality on `α`, and any elements `a` of type `α` and `b` of type `β a`, and any two functions `f, g : (a : α) → β a`, the function `g` is equal to the function `f` updated at `a` with `b` if and only if the value of `g` at `a` is `b` and for all `x` in `α` such that `x` is not equal to `a`, the value of `g` at `x` is equal to the value of `f` at `x`. In other words, this theorem states the condition under which a function equals another function with one of its values updated.
More concisely: For functions `f` and `g` over a type `α` where `β` is type dependent on `α`, `g` equals `f` updated at `a` with `b` if and only if `g a = b` and for all `x ≠ a`, `g x = f x`.
|
Function.Surjective.forall₃
theorem Function.Surjective.forall₃ :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β},
Function.Surjective f →
∀ {p : β → β → β → Prop}, (∀ (y₁ y₂ y₃ : β), p y₁ y₂ y₃) ↔ ∀ (x₁ x₂ x₃ : α), p (f x₁) (f x₂) (f x₃)
The theorem `Function.Surjective.forall₃` states that for any type `α` and `β` and any function `f` from `α` to `β`, if `f` is surjective, then for any predicate `p` that takes three arguments of type `β`, the predicate `p` holds for any three elements of type `β` if and only if `p` holds for the images of any three elements of type `α` under the function `f`. In other words, we can replace any three elements of type `β` in the predicate `p` by their preimages in type `α` under the function `f`, without changing the truth value of `p`, provided `f` is surjective.
More concisely: If `f: α → β` is a surjective function, then for any predicate `p:` `β → Prop`, `p` holds for any three elements of `β` if and only if `p` holds for the images of any three elements of `α` under `f`.
|
Function.extend_apply'
theorem Function.extend_apply' :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (g : α → γ) (e' : β → γ) (b : β),
(¬∃ a, f a = b) → Function.extend f g e' b = e' b
This theorem `Function.extend_apply'` states that for any types `α`, `β`, and `γ`, and any functions `f : α → β`, `g : α → γ`, and `e' : β → γ`, and for any value `b : β`, if there does not exist a value `a : α` such that `f a = b`, then the function `Function.extend f g e'` applied to `b` equals `e' b`. In simpler terms, this theorem describes a condition under which the extension of a function `f` behaves like the function `e'` for a particular value `b`.
More concisely: If `f : α → β` has no preimage under `b : β`, then `Function.extend f g e' b = e' b`.
|
Function.Surjective.of_comp
theorem Function.Surjective.of_comp :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α},
Function.Surjective (f ∘ g) → Function.Surjective f
The theorem `Function.Surjective.of_comp` states that for all types `α`, `β`, and `γ`, and for all functions `f` from `α` to `β` and `g` from `γ` to `α`, if the composition of `f` with `g` (denoted as `f ∘ g`) is surjective, then `f` itself is also surjective. In mathematical terms, if for every element in the codomain type `β` there exists an element in the domain type `γ` such that applying the composed function `f ∘ g` to it results in the element in `β`, then for every element in `β`, there exists an element in `α` such that applying `f` to it results in that element in `β`.
More concisely: If the composition of functions `f : α → β` and `g : γ → α` is surjective, then `f` is surjective.
|
Function.Involutive.ite_not
theorem Function.Involutive.ite_not :
∀ {α : Sort u} {f : α → α},
Function.Involutive f →
∀ (P : Prop) [inst : Decidable P] (x : α), f (if P then x else f x) = if ¬P then x else f x
The theorem `Function.Involutive.ite_not` states that for any type `α`, for any function `f` from `α` to `α`, if `f` is involutive (i.e., if applying `f` twice to any value gives back the original value), then for any proposition `P` and any value `x` of type `α`, applying `f` to the value obtained by choosing between `x` and `f x` based on `P` (using the 'if then else' construct) gives the same value as choosing between `x` and `f x` based on the negation of `P`. This shows that an involutive function can 'flip' the condition in an 'if then else' construct.
More concisely: For any involutive function `f` from type `α` to itself and any proposition `P` and value `x` of type `α`, `(if P then f else id) x = if (≠P) then id else f x`.
|
Function.Injective2.right
theorem Function.Injective2.right :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ},
Function.Injective2 f → ∀ (a : α), Function.Injective (f a)
The theorem `Function.Injective2.right` states that for all types `α`, `β`, and `γ`, and for any binary function `f : α → β → γ`, if `f` is injective in both arguments (meaning that if `f a₁ b₁ = f a₂ b₂`, then `a₁ = a₂` and `b₁ = b₂`), then `f` is also injective in its second argument when the first argument is fixed. In other words, for every fixed value of `a : α`, the function `f a` is injective, which means that if `f a b₁ = f a b₂`, then `b₁ = b₂`.
More concisely: If a binary function `f : α → β → γ` is injective in both arguments, then for every fixed `a : α`, the function `f a : β → γ` is injective.
|
Function.sometimes_spec
theorem Function.sometimes_spec :
∀ {p : Prop} {α : Sort u_1} [inst : Nonempty α] (P : α → Prop) (f : p → α) (a : p),
P (f a) → P (Function.sometimes f)
The theorem `Function.sometimes_spec` asserts that for any proposition `p`, any type `α` that is nonempty, any property `P` from `α` to a proposition, any function `f` from `p` to `α`, and any instance `a` of the proposition `p`, if the property `P` holds for the result of applying `f` to `a`, then the property `P` also holds for `Function.sometimes f`. In other words, if `P(f(a))` is true, then `P(Function.sometimes f)` is also true. This theorem is particularly useful when we want to establish that a property holds for some value of a function, without specifying exactly what that value is.
More concisely: If for any proposition `p`, nonempty type `α`, property `P` from `α` to a proposition, function `f` from `p` to `α`, and instance `a` of `p` with `P(f(a))`, then `P(Function.sometimes f)` holds.
|
Function.Injective.eq_iff
theorem Function.Injective.eq_iff :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Injective f → ∀ {a b : α}, f a = f b ↔ a = b
The theorem `Function.Injective.eq_iff` states that for any types `α` and `β`, and for any function `f` from `α` to `β`, if `f` is injective (that is, `f x = f y` implies `x = y`), then for all elements `a` and `b` of `α`, `f a` is equal to `f b` if and only if `a` is equal to `b`. In other words, the equality of function outputs is equivalent to the equality of inputs for an injective function.
More concisely: For any function `f:` X → Y between types X and Y, `f` being injective (i.e., `f x = f y` implies `x = y`) is equivalent to `x = y` if and only if `f x = f y`.
|
Function.Involutive.surjective
theorem Function.Involutive.surjective : ∀ {α : Sort u} {f : α → α}, Function.Involutive f → Function.Surjective f := by
sorry
The theorem `Function.Involutive.surjective` states that for any type `α` and any function `f : α → α`, if `f` is involutive (meaning that applying `f` twice to any element gives you back the original element, i.e., `f ∘ f = id`), then `f` is also surjective. In terms of mathematics, this means that for any `α` in the universe of discourse and any function `f : α → α`, if `f` is such that `f(f(x)) = x` for all `x` in `α`, then for every `y` in `α`, there exists an `x` in `α` such that `f(x) = y`.
More concisely: If `f : α → α` is an involutive function (`f ∘ f = id`), then `f` is surjective (for every `y` in `α`, there exists an `x` in `α` such that `f(x) = y`).
|
Function.surjInv_eq
theorem Function.surjInv_eq :
∀ {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f) (b : β), f (Function.surjInv h b) = b := by
sorry
The theorem `Function.surjInv_eq` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, if `f` is surjective (meaning that for every element `b` in `β`, there exists some element `a` in `α` such that `f(a) = b`), then applying `f` to the inverse of `f` (as determined by the surjectivity proof `h`), when given any element `b` from `β`, equals `b`. The inverse function here, `Function.surjInv h b`, gives an element `a` in `α` such that `f(a) = b` for a given `b` in `β`, based on the surjective nature of `f`. The theorem thus essentially verifies the correctness of the surjective inverse function.
More concisely: For all types `α` and `β` and surjective functions `f` from `α` to `β`, `f (Function.surjInv f b) = b` for all `b` in `β`.
|
Function.Surjective.injective_comp_right
theorem Function.Surjective.injective_comp_right :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
Function.Surjective f → Function.Injective fun g => g ∘ f
The theorem `Function.Surjective.injective_comp_right` states that for all types `α`, `β`, and `γ` and for every function `f` from `α` to `β`, if function `f` is surjective, then the function given by composition with `f` on the right, i.e., the function `g ↦ g ∘ f` for a function `g : β → γ`, is injective. This means that if every element in the codomain `β` is mapped from some element in the domain `α` by the function `f`, then for any two different functions `g₁` and `g₂` from `β` to `γ`, their compositions with `f` are also different. In mathematical terms, if `f` is surjective and `g₁ ∘ f = g₂ ∘ f`, then `g₁ = g₂`.
More concisely: If `f : α → β` is surjective, then for every `γ-valued` function `g₁ ≠ g₂`, the functions `g₁ ∘ f` and `g₂ ∘ f` are distinct.
|
Function.cantor_surjective
theorem Function.cantor_surjective : ∀ {α : Type u_4} (f : α → Set α), ¬Function.Surjective f
**Cantor's diagonal argument theorem** states that for any type `α`, there cannot exist a function from `α` to the set of all subsets of `α` (`Set α`) that is surjective. In other words, there is no function that, for every subset of `α`, there is an element of `α` that the function maps to that subset. This theorem is a result of Cantor's diagonal argument, a fundamental concept in set theory and theory of computation.
More concisely: There does not exist a surjective function from any type `α` to the power set `Set α`.
|
Function.Injective.hasLeftInverse
theorem Function.Injective.hasLeftInverse :
∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β}, Function.Injective f → Function.HasLeftInverse f
The theorem `Function.Injective.hasLeftInverse` states that for every function `f` from a nonempty type `α` to any type `β`, if `f` is injective (meaning that identical outputs imply identical inputs), then `f` has a left inverse. In mathematical terms, this left inverse is a function that, when composed with `f` from the left, results in the identity function on `α`.
More concisely: If `f: α → β` is injective, then there exists a function `g: β → α` such that `f ∘ g = idα`.
|
Function.update_noteq
theorem Function.update_noteq :
∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] {a a' : α},
a ≠ a' → ∀ (v : β a') (f : (a : α) → β a), Function.update f a' v a = f a
This theorem, `Function.update_noteq`, states that for any type `α` with decidable equality, any type mapping `β : α → Sort v`, and any two elements `a` and `a'` of type `α` that are not equal, for any value `v : β a'` and any function `f : (a : α) → β a`, the result of updating the function `f` at point `a'` with value `v` and then evaluating it at point `a` is the same as the original value of the function `f` at point `a`. In simpler terms, if you update the value of a function at a point and then evaluate the function at a different point, the output of the function doesn't change.
More concisely: For any type `α` with decidable equality, any type mapping `β : α → Sort v`, and functions `f : α → β`, `a`, `a' : α (a ≠ a')`, the value `f a` is equal to `(Function.update f a' v) a`.
|
Function.Injective2.right'
theorem Function.Injective2.right' :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ},
Function.Injective2 f → ∀ [inst : Nonempty α], Function.Injective fun b a => f a b
The theorem `Function.Injective2.right'` states that for all types α, β, and γ, and a binary function `f` from α and β to γ, if `f` is injective as a binary function (i.e., if for all pairs of elements `a1`, `a2` from α and `b1`, `b2` from β, if `f a1 b1` equals `f a2 b2`, then `a1` equals `a2` and `b1` equals `b2`), then, provided that α is nonempty, `f` is also injective as a unary function when viewed as a map from β to γ that is parameterized over some fixed element of α. This means that if we fix some value `a` in α, and for all `b1`, `b2` in β, if `f a b1` equals `f a b2`, then `b1` equals `b2`.
More concisely: If a binary function `f` from types α and β to γ is injective, then for any fixed `a` in α, the unary function `x mapsto f a x` from β to γ is also injective.
|
Function.Injective.ne_iff'
theorem Function.Injective.ne_iff' :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β},
Function.Injective f → ∀ {x y : α} {z : β}, f y = z → (f x ≠ z ↔ x ≠ y)
This theorem states that for all types `α` and `β`, if a function `f` from `α` to `β` is injective (i.e., no two different elements in `α` map to the same element in `β`), then for any elements `x` and `y` in `α` and `z` in `β`, if `f y` equals `z`, then `f x` is not equal to `z` if and only if `x` is not equal to `y`. In other words, in the context of an injective function, `x` and `y` being distinct guarantees that their images under `f` will also be distinct.
More concisely: For all types `α` and `β`, if `f : α → β` is injective, then for all `x`, `y` in `α` and `z` in `β`, `f x = z` implies `x = y` or `f y ≠ z`.
|
Function.update_eq_const_of_subsingleton
theorem Function.update_eq_const_of_subsingleton :
∀ {α : Sort u} {α' : Sort w} [inst : DecidableEq α] [inst_1 : Subsingleton α] (a : α) (v : α') (f : α → α'),
Function.update f a v = Function.const α v
This theorem, named `Function.update_eq_const_of_subsingleton`, states that for any types `α` and `α'` with equality on `α` being decidable, if `α` is a subsingleton type (a type with at most one element), then the function `f : α → α'` updated at any point `a : α` to a value `v : α'` is equivalent to the constant function with value `v`. In other words, if there is at most one possible input to a function, updating the function at that input doesn't change the overall function; it just results in a constant function.
More concisely: For any type `α` with decidable equality and being a subsingleton, the function `f : α → α'` is equal to the constant function `Const v : α → α'` for any `v : α'`.
|
Function.Surjective.hasRightInverse
theorem Function.Surjective.hasRightInverse :
∀ {α : Sort u} {β : Sort v} {f : α → β}, Function.Surjective f → Function.HasRightInverse f
The theorem `Function.Surjective.hasRightInverse` states that for every function `f` from a set (or type) `α` to a set `β`, if `f` has the property of being surjective (that is, for every element `b : β`, there exists an element `a : α` such that `f(a) = b`), then `f` also has a right inverse. A right inverse of `f` is another function `finv` such that applying `f` and then `finv` to any element of `β` returns that element, i.e., `f(finv(b)) = b` for all `b` in `β`.
More concisely: If `f` is a surjective function from `α` to `β`, then there exists a right inverse `finv` for `f` such that `f(finv(b)) = b` for all `b` in `β`.
|
Function.Involutive.eq_iff
theorem Function.Involutive.eq_iff :
∀ {α : Sort u} {f : α → α}, Function.Involutive f → ∀ {x y : α}, f x = y ↔ x = f y
This theorem states that for any type `α` and function `f` from `α` to `α`, if `f` is involutive (i.e., applying `f` twice returns the original value: `f(f(x)) = x`), then for any two elements `x` and `y` of `α`, `f(x) = y` if and only if `x = f(y)`. This means that if function `f` is an involution, it commutes across an equality, which is similar to the property of injective functions where if the outputs are the same, then the inputs are the same.
More concisely: An involutive function `f` over type `α` satisfies `x = y` if and only if `f(x) = f(y)`.
|
Function.Injective2.left
theorem Function.Injective2.left :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ},
Function.Injective2 f → ∀ (b : β), Function.Injective fun a => f a b
The theorem `Function.Injective2.left` states that for all types `α`, `β`, and `γ`, and for all binary functions `f` from `α` and `β` to `γ`, if `f` is binary injective (meaning that for any pairs of elements `a₁, a₂` in `α` and `b₁, b₂` in `β`, if `f(a₁, b₁)` equals `f(a₂, b₂)`, then `a₁` equals `a₂` and `b₁` equals `b₂`), then for any fixed `b` in `β`, the function that varies only in the `α` element (defined as `a` maps to `f a b`) is also injective (meaning that for any `a₁, a₂` in `α`, if `f(a₁, b)` equals `f(a₂, b)`, then `a₁` equals `a₂`). This theorem essentially establishes that holding one variable constant in a binary injective function results in an injective function of the remaining variable.
More concisely: If a binary function `f` from `α × β` to `γ` is injective, then for each fixed `b` in `β`, the restriction of `f` to `α` is also injective.
|
Function.Injective2.eq_iff
theorem Function.Injective2.eq_iff :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ},
Function.Injective2 f → ∀ {a₁ a₂ : α} {b₁ b₂ : β}, f a₁ b₁ = f a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂
This theorem states that for any binary function `f : α → β → γ`, if `f` is injective (in the sense that if `f a₁ b₁ = f a₂ b₂` then `a₁ = a₂` and `b₁ = b₂`), then for any `a₁, a₂` in `α` and `b₁, b₂` in `β`, `f a₁ b₁ = f a₂ b₂` if and only if `a₁ = a₂` and `b₁ = b₂`. In other words, the binary function `f` being injective is equivalent to the condition that the equality of function outputs `f a₁ b₁` and `f a₂ b₂` implies and is implied by the equality of the corresponding inputs `(a₁, b₁)` and `(a₂, b₂)`.
More concisely: If `f : α → β → γ` is an injective function, then for all `a₁, a₂ in α` and `b₁, b₂ in β`, `f a₁ b₁ = f a₂ b₂` if and only if `(a₁, b₁) = (a₂, b₂)`.
|
Function.hfunext
theorem Function.hfunext :
∀ {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : (a : α) → β a} {f' : (a : α') → β' a},
α = α' → (∀ (a : α) (a' : α'), HEq a a' → HEq (f a) (f' a')) → HEq f f'
This theorem, `Function.hfunext`, in Lean 4, states that given two function types `f : (a : α) → β a` and `f' : (a : α') → β' a'`, where `α` and `α'` are sorts and `β` and `β'` are type-level functions, if `α` is exactly the same as `α'` and for all `a` in `α` and `a'` in `α'`, if `a` and `a'` are propositionally equal (using heterogeneous equality `HEq`), then the result of the function `f` applied to `a` and the function `f'` applied to `a'` are also propositionally equal, we can conclude that the functions `f` and `f'` themselves are propositionally equal. This theorem is a generalization of function extensionality to heterogeneous types.
More concisely: Given two functions `f : α → β` and `f' : α' → β'` between heterogeneous types `α`, `α'`, `β`, and `β'`, if `α = α'`, `HEq (a : α) (a' : α')`, and `β f a = β' (f' a')`, then `f = f'`.
|
Function.ne_iff
theorem Function.ne_iff : ∀ {α : Sort u_1} {β : α → Sort u_4} {f₁ f₂ : (a : α) → β a}, f₁ ≠ f₂ ↔ ∃ a, f₁ a ≠ f₂ a := by
sorry
This theorem, `Function.ne_iff`, states that for all sorts `α` and `β` that is a function of `α`, and for all functions `f₁` and `f₂` from `α` to `β`, `f₁` is not equal to `f₂` if and only if there exists an element `a` in `α` such that `f₁ a` is not equal to `f₂ a`. In other words, two functions are different if and only if there is at least one argument for which they yield different results.
More concisely: For functions between types `α` and `β`, `f₁` is not equal to `f₂` if and only if there exists an `x ∈ α` such that `f₁ x ≠ f₂ x`.
|
Function.Bijective.surjective
theorem Function.Bijective.surjective :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Bijective f → Function.Surjective f
The theorem `Function.Bijective.surjective` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, if the function `f` is bijective (that is, it is both injective and surjective), then the function `f` is also surjective. In other words, a bijective function is always a surjective function. Surjectivity means that for every element `b` in the codomain `β`, there exists an element `a` in the domain `α` such that `f(a) = b`.
More concisely: If a function between types is bijective, then it is surjective.
|
Function.Surjective.forall₂
theorem Function.Surjective.forall₂ :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β},
Function.Surjective f → ∀ {p : β → β → Prop}, (∀ (y₁ y₂ : β), p y₁ y₂) ↔ ∀ (x₁ x₂ : α), p (f x₁) (f x₂)
The theorem `Function.Surjective.forall₂` states that for any given types `α` and `β` and any function `f : α → β`, if the function `f` is surjective (i.e., for every element `b` in `β`, there exists an element `a` in `α` such that `f(a) = b`), then for any given property `p` that relates two elements in `β`, `p` holds for all pairs of elements in `β` if and only if `p` holds for all pairs of elements in `α` mapped by the function `f`. In other words, we can check the property `p` on the image of `f` instead of the entire codomain `β` if `f` is surjective.
More concisely: If `f : α → β` is a surjective function, then `p(a₁, a₂) ↔ p(f a₁, f a₂)` for any binary relation `p : β → β → Prop`.
|
Function.leftInverse_invFun
theorem Function.leftInverse_invFun :
∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β},
Function.Injective f → Function.LeftInverse (Function.invFun f) f
The theorem `Function.leftInverse_invFun` states that for any types `α` and `β` and a function `f` from `α` to `β`, if `α` is nonempty and `f` is an injective function, then the inverse function `Function.invFun f` is a left inverse to `f`. In other words, if `f` is a function that does not map different elements of `α` to the same element of `β`, then applying `f` and then its inverse will return the original value for all elements in `α`, i.e., `(Function.invFun f) ∘ f = id`.
More concisely: If `f` is an injective function from a nonempty `α` to `β`, then `Function.invFun f ∘ f = id`.
|
Function.Injective.eq_iff'
theorem Function.Injective.eq_iff' :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β},
Function.Injective f → ∀ {a b : α} {c : β}, f b = c → (f a = c ↔ a = b)
This theorem states that for any types `α` and `β`, and any function `f` from `α` to `β`, if `f` is injective (meaning that `f` maps distinct inputs to distinct outputs), then for any two elements `a` and `b` of `α` and any element `c` of `β`, if `f b = c`, then `f a = c` if and only if `a = b`. In simpler terms, if an injective function `f` maps `b` to `c`, then it also maps `a` to `c` if and only if `a` and `b` are the same.
More concisely: If `f` is an injective function from type `α` to type `β`, then for all `a, b : α` and `c : β`, if `f b = c`, then `a = b` implies `f a = c`.
|
Function.LeftInverse.comp
theorem Function.LeftInverse.comp :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β},
Function.LeftInverse f g → Function.LeftInverse h i → Function.LeftInverse (h ∘ f) (g ∘ i)
The theorem `Function.LeftInverse.comp` states that given two pairs of functions `(f, g)` and `(h, i)` where `g` is a left inverse to `f` and `i` is a left inverse to `h`, the composition of `h` and `f` also has a left inverse, which is the composition of `g` and `i`. In other words, if `g ∘ f = id` and `i ∘ h = id`, then `(g ∘ i) ∘ (h ∘ f) = id`. This asserts the composability of left inverses in function composition.
More concisely: If functions `f` and `g`, and `h` and `i` are pairs with `g` a left inverse of `f` and `i` a left inverse of `h`, then `g ∘ i` is a left inverse of their composite `h ∘ f`.
|
Function.leftInverse_surjInv
theorem Function.leftInverse_surjInv :
∀ {α : Sort u} {β : Sort v} {f : α → β} (hf : Function.Bijective f), Function.LeftInverse (Function.surjInv ⋯) f
The theorem `Function.leftInverse_surjInv` states that for all sorts `α` and `β`, and for any function `f` from `α` to `β`, if `f` is bijective (both injective and surjective), then the function `Function.surjInv` is a left inverse to `f`. In other words, if we have a bijective function `f`, then applying `f` and then `Function.surjInv` (in this order) to any element of `α` will return that very same element. This theorem essentially shows that we can retrieve the original value from any bijective function using its surjective inverse.
More concisely: If `f` is a bijective function from `α` to `β`, then `Function.surjInv ∘ f = id` (where `id` is the identity function on `α`).
|
Function.update_same
theorem Function.update_same :
∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (a : α) (v : β a) (f : (a : α) → β a),
Function.update f a v a = v
This theorem, "Function.update_same", states that for any type `α` with decidable equality, any function `f` from `α` to some type `β` dependent on `α`, and any value `a` of type `α` and `v` of type `β a`, if we update the function `f` at `a` to be `v`, then the value of the updated function at `a` is `v`. In other words, if we replace the value of a function at a given point by a certain value, then the function at that point yields the new value.
More concisely: For any type `α` with decidable equality and function `f` from `α` to type `β`, if `a : α` and `v : β (a)`, then updating `f` at `a` to `v` results in a function `g` such that `g a = v`.
|
Function.cantor_injective
theorem Function.cantor_injective : ∀ {α : Type u_4} (f : Set α → α), ¬Function.Injective f
**Cantor's Diagonal Argument Theorem** states that for any type `α`, there cannot exist an injective function `f` that maps from the set of all subsets of `α` (`Set α`) to `α` itself. In other words, there is no function `f` such that for every two different subsets of `α`, the function `f` gives two different elements of `α`. This theorem is a direct application of Cantor's diagonal argument, which demonstrates the uncountability of the set of all subsets of a countable set.
More concisely: There does not exist an injective function from the set of all subsets of a type `α` to `α` itself.
|
Function.id_def
theorem Function.id_def : ∀ {α : Sort u_1}, id = fun x => x
This theorem states that for all types `α`, the identity function `id` is equivalent to the function that takes an input `x` and returns `x`. In other words, the theorem formalizes the definition of the identity function: a function that returns its input unchanged.
More concisely: For all types `α`, the identity function `id : α → α` is equal to the function that maps each `x : α` to `x`.
|
Function.Injective.comp_left
theorem Function.Injective.comp_left :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ},
Function.Injective g → Function.Injective fun x => g ∘ x
The theorem `Function.Injective.comp_left` states that if you have a function `g : β → γ` that is injective (meaning for any two elements `x` and `y` in `β`, if `g(x)` is equal to `g(y)`, then `x` must be equal to `y`), then the function that takes another function `x : α → β` and returns the composition of `g` and `x` (denoted as `g ∘ x`) is also injective. In other words, composition by an injective function on the left preserves injectivity.
More concisely: If `g : β → γ` is an injective function, then the function `g ∘ x` is injective for all functions `x : α → β`.
|
Function.Bijective.existsUnique_iff
theorem Function.Bijective.existsUnique_iff :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Bijective f → ∀ {p : β → Prop}, (∃! y, p y) ↔ ∃! x, p (f x)
The theorem `Function.Bijective.existsUnique_iff` states that for any two types `α` and `β` and a function `f` from `α` to `β`, if `f` is bijective, then for any property `p` satisfied by elements of `β`, there exists a unique `y` in `β` such that `p(y)` is true if and only if there exists a unique `x` in `α` such that `p(f(x))` is true. In other words, a property uniquely holds for an element in the codomain of a bijective function if and only if it uniquely holds for its preimage in the domain.
More concisely: For a bijective function `f` from `α` to `β`, a property `p` holds uniquely for an element `y` in `β` if and only if it holds uniquely for the preimage `x` in `α` such that `f(x) = y`.
|
Function.Bijective.injective
theorem Function.Bijective.injective :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Bijective f → Function.Injective f
This theorem states that for any types `α` and `β`, and for any function `f` from `α` to `β`, if `f` is bijective (which means it is both injective and surjective), then `f` is also injective. In other words, if a function maps distinct elements of the domain to distinct elements of the codomain and every element of the codomain is the image of some element of the domain, then it must be the case that the same output from the function implies that the inputs were the same.
More concisely: If `f` is a function from type `α` to type `β` that is bijective, then `f` is injective.
|
Function.RightInverse.injective
theorem Function.RightInverse.injective :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.RightInverse f g → Function.Injective f := by
sorry
The theorem `Function.RightInverse.injective` states that for any two types `α` and `β`, and any two functions `f : α → β` and `g : β → α`, if `g` is a right inverse to `f` (that is, composing `f` and `g` results in the identity function), then `f` is an injective function. In other words, if `f(g(x)) = x` for all `x` in `β`, then for any `x1` and `x2` in `α`, if `f(x1) = f(x2)` then `x1 = x2`.
More concisely: If a function `f : α → β` has a right inverse `g : β → α` (i.e., `f ∘ g = idβ` and `g ∘ f = idα`), then `f` is an injective function (i.e., `f x₁ = f x₂` implies `x₁ = x₂` for all `x₁, x₂ : α`).
|
Function.Involutive.leftInverse
theorem Function.Involutive.leftInverse :
∀ {α : Sort u} {f : α → α}, Function.Involutive f → Function.LeftInverse f f
The theorem `Function.Involutive.leftInverse` states that for any type `α` and any function `f : α → α`, if `f` is an involutive function (meaning that applying `f` twice to any element gives back the original element, i.e., `f ∘ f = id`), then `f` is its own left inverse. In other words, `f` composed with itself equals the identity function, which can be written as `f ∘ f = id`.
More concisely: If a function `f : α → α` is involutive (i.e., `f ∘ f = id`), then `f` is its own left inverse (i.e., `f ∘ f = id = id ∘ f`).
|
Function.Injective.of_comp_iff
theorem Function.Injective.of_comp_iff :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
Function.Injective f → ∀ (g : γ → α), Function.Injective (f ∘ g) ↔ Function.Injective g
The theorem `Function.Injective.of_comp_iff` states that for any types `α`, `β`, and `γ`, and any function `f` from `α` to `β`, if `f` is injective, then for any function `g` from `γ` to `α`, `f ∘ g` (the composition of `f` and `g`) is injective if and only if `g` is injective. In other words, when composing with an injective function, the injectivity of the resulting function is equivalent to the injectivity of the original function.
More concisely: If `f: α -> β` is injective, then `f ∘ g: γ -> β` is injective if and only if `g: γ -> α` is injective.
|
Function.update_injective
theorem Function.update_injective :
∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (f : (a : α) → β a) (a' : α),
Function.Injective (Function.update f a')
The theorem `Function.update_injective` states that, for any type `α` with decidable equality and any dependent type `β` over `α`, and any function `f : α → β a`, and any element `a' : α`, the function update operation `Function.update f a'` is injective. In other words, if you update the value of the function `f` at some point `a'`, then this new function will not map different inputs to the same output. If two inputs produce the same output, then they were the same input initially. This holds under the condition that the equality of elements in `α` is decidable.
More concisely: Given a type `α` with decidable equality, and a function `f : α → β` from `α` to another type `β`, the updated function `Function.update f a'` is a injection (one-to-one function) for any `a' : α`.
|
Function.Surjective.forall
theorem Function.Surjective.forall :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β},
Function.Surjective f → ∀ {p : β → Prop}, (∀ (y : β), p y) ↔ ∀ (x : α), p (f x)
The theorem `Function.Surjective.forall` states that for all types `α` and `β` and for any function `f` from `α` to `β`, if `f` is surjective, then for any property `p` defined on `β`, `p` holds for all elements of `β` if and only if `p` holds for all elements of `α` when applied to `f(x)`. In other words, a property is true for all of `β` if it is true for all of the images of `α` under a surjective function `f`.
More concisely: If `f : α → β` is a surjective function, then for any property `p` on `β`, `∀x ∈ β, p(x) ↔ ∀x ∈ α, p(f(x))`.
|
Function.surjective_eval
theorem Function.surjective_eval :
∀ {α : Sort u} {β : α → Sort v} [h : ∀ (a : α), Nonempty (β a)] (a : α), Function.Surjective (Function.eval a) := by
sorry
The theorem `Function.surjective_eval` states that for every type `α` and a type family `β` indexed over `α`, assuming that for every element `a : α`, there is at least one element of type `β a` (`Nonempty (β a)`), then for any element `a : α`, the function `Function.eval a` is surjective. In other words, for any element `b` of the type `β a`, there exists a function such that when this function is applied to `a`, it yields `b`.
More concisely: Given a type `α` and a type family `β : α → Prop` such that for every `a : α`, there exists `b : β a`, the evaluation map `Function.eval : ∀ (f : α → β), f a ∈ β a → β` is surjective.
|
Function.LeftInverse.surjective
theorem Function.LeftInverse.surjective :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.LeftInverse f g → Function.Surjective f := by
sorry
The theorem `Function.LeftInverse.surjective` states that for all types `α` and `β`, and for all functions `f` from `α` to `β` and `g` from `β` to `α`, if `f` is a left inverse to `g` (i.e., for all `x` in `α`, `f(g(x)) = x`), 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 left inverse `g : β → α` (i.e., `g ∘ f = idα`), then `f` is surjective.
|
Function.injective_of_subsingleton
theorem Function.injective_of_subsingleton :
∀ {α : Sort u_1} {β : Sort u_2} [inst : Subsingleton α] (f : α → β), Function.Injective f
The theorem `Function.injective_of_subsingleton` states that for any two types `α` and `β`, and any function `f` from `α` to `β`, if `α` is a subsingleton type (meaning it has at most one element), then the function `f` is injective. In other words, if the elements of `α` are identical or there is only one element, then each element of `β` is mapped by `f` from at most one element of `α`.
More concisely: If `α` is a subsingleton type, then any function `f` from `α` to `β` is injective.
|
Function.Injective.of_comp_iff'
theorem Function.Injective.of_comp_iff' :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α},
Function.Bijective g → (Function.Injective (f ∘ g) ↔ Function.Injective f)
This theorem states that for all types `α`, `β`, and `γ`, and given a function `f` from `α` to `β`, and a bijective function `g` from `γ` to `α`, the composition of `f` and `g` (denoted as `f ∘ g`) is injective if and only if `f` itself is injective. In other words, when `g` is a bijective mapping, the injectiveness of the composed function `f ∘ g` is equivalent to the injectiveness of the original function `f`.
More concisely: For all types `α`, `β`, and `γ`, if `f: α → β` is injective and `g: γ → α` is bijective, then their composition `f ∘ g: γ → β` is also injective.
|
Function.Injective.ne_iff
theorem Function.Injective.ne_iff :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Injective f → ∀ {x y : α}, f x ≠ f y ↔ x ≠ y
The theorem `Function.Injective.ne_iff` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, if `f` is injective (meaning that equal outputs imply equal inputs), then for any two elements `x` and `y` of `α`, the inequality `f(x) ≠ f(y)` is equivalent to `x ≠ y`. In other words, the function does not give the same output for two different inputs, if and only if those inputs are actually different.
More concisely: For any function between types, injectivity is equivalent to the condition that distinct inputs map to distinct outputs.
|
Function.extend_def
theorem Function.extend_def :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (g : α → γ) (e' : β → γ) (b : β)
[inst : Decidable (∃ a, f a = b)],
Function.extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b
The theorem `Function.extend_def` is about the definition of the function `Function.extend` for any given types `α`, `β` and `γ`, and functions `f : α → β`, `g : α → γ` and `e' : β → γ`, and a value `b : β`. If it is decidable whether there exists an `a` such that `f a = b`, then `Function.extend f g e' b` is defined as follows: if there exists such an `a`, then it is `g (Classical.choose h)`, where `h` is the proof of existence. Otherwise, it is `e' b`. Here, `Classical.choose` is a function that given a proof of existence of a value satisfying a property, gives you a specific value satisfying that property.
More concisely: Given functions `f : α -> β`, `g : α -> γ`, `e' : β -> γ`, and `b : β`, if it is decidable which `a : α` satisfies `f a = b`, then `Function.extend f g e' b` is `g (the a | exists a, f a = b)` or `e' b` otherwise.
|
Function.Bijective.of_comp_iff
theorem Function.Bijective.of_comp_iff :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α},
Function.Bijective g → (Function.Bijective (f ∘ g) ↔ Function.Bijective f)
This theorem states that for all types `α`, `β`, and `γ` and for all functions `f : α → β` and `g : γ → α`, if `g` is bijective (i.e., it is both injective and surjective), then the composition of `f` and `g` (denoted as `f ∘ g`) is bijective if and only if `f` itself is bijective.
More concisely: If `f : α → β` and `g : γ → α` are functions with `g` bijective, then `f ∘ g` is bijective if and only if `f` is bijective.
|
Function.Bijective.comp_left
theorem Function.Bijective.comp_left :
∀ {α : Sort u} {β : Sort v} {γ : Sort w} {g : β → γ}, Function.Bijective g → Function.Bijective fun x => g ∘ x := by
sorry
This theorem states that, given any three sets `α`, `β`, and `γ`, if a function `g` from `β` to `γ` is bijective, then the composition of `g` with any function from `α` to `β` is also bijective. In other words, if `g` is a one-to-one correspondence between `β` and `γ`, then applying `g` after any function from `α` to `β` also results in a one-to-one correspondence. This theorem is a fundamental result in the theory of functions.
More concisely: If `g` is a bijective function from `β` to `γ`, then the composition `f ∘ g` is bijective for any function `f` from `α` to `β`.
|
Function.Involutive.rightInverse
theorem Function.Involutive.rightInverse :
∀ {α : Sort u} {f : α → α}, Function.Involutive f → Function.RightInverse f f
The theorem `Function.Involutive.rightInverse` states that for any type `α` and any function `f` from `α` to `α`, if `f` is involutive (meaning applying `f` twice to any input yields the original input), then `f` is also a right inverse to itself. That is, composing `f` with itself yields the identity function. In mathematical terms, if for all `x` in `α`, `f(f(x)) = x`, then `f ∘ f = id`, where `id` is the identity function.
More concisely: If a function `f` from type `α` to `α` is involutive (i.e., `f(f(x)) = x` for all `x` in `α`), then `f` is its own right inverse (i.e., `f ∘ f = id`).
|
Function.Injective.of_comp
theorem Function.Injective.of_comp :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α},
Function.Injective (f ∘ g) → Function.Injective g
The theorem `Function.Injective.of_comp` states that for all types `α`, `β`, and `γ`, and for all functions `f` from `α` to `β` and `g` from `γ` to `α`, if the composite function `f ∘ g` (meaning `f` after `g`) is injective (i.e., it never maps distinct inputs to the same output), then the function `g` is also injective. This is a property of function composition in mathematical logic.
More concisely: If `f ∘ g` is injective for functions `f: α -> β` and `g: γ -> α`, then `g` is injective.
|
Function.apply_update₂
theorem Function.apply_update₂ :
∀ {ι : Sort u_1} [inst : DecidableEq ι] {α : ι → Sort u_2} {β : ι → Sort u_3} {γ : ι → Sort u_4}
(f : (i : ι) → α i → β i → γ i) (g : (i : ι) → α i) (h : (i : ι) → β i) (i : ι) (v : α i) (w : β i) (j : ι),
f j (Function.update g i v j) (Function.update h i w j) =
Function.update (fun k => f k (g k) (h k)) i (f i v w) j
The theorem `Function.apply_update₂` states that for any indices of type `ι` where `ι` has decidable equality, and any functions `f`, `g`, and `h` with appropriate types, updating the values of `g` and `h` at a certain index `i` to `v` and `w` respectively, and then applying `f` at index `j` to the updated `g` and `h`, is the same as updating the function `(fun k => f k (g k) (h k))` at index `i` to `f i v w` and then applying this updated function at index `j`.
In simpler terms, this theorem is about the commutativity of the "update" operation with the function application. It tells us that one can either first update the inputs of a function and then apply the function, or first apply the function on the original inputs and then update the results, and these two processes will give the same output.
More concisely: For functions `f`, `g`, and `h` with decidable domain `ι`, and any indices `i` and `j`, the update of `g` and `h` at `i` to `v` and `w`, followed by applying `f` at index `j`, is equivalent to applying `f` at index `j` to the original `g` and `h`, then updating the result of `f` at index `i` to `f i v w`.
|
Function.Involutive.bijective
theorem Function.Involutive.bijective : ∀ {α : Sort u} {f : α → α}, Function.Involutive f → Function.Bijective f := by
sorry
The theorem `Function.Involutive.bijective` states that for any type `α` and any function `f` from `α` to `α`, if `f` is involutive (i.e., applying `f` twice to any element `x` in `α` yields `x` back, formally `f ∘ f = id`), then `f` is bijective. A bijective function is both injective (each element of the domain maps to a unique element of the codomain) and surjective (every element of the codomain is mapped to by some element of the domain).
More concisely: If a function from a type to itself is involutive (i.e., self-inverse), then it is bijective.
|
Function.rightInverse_surjInv
theorem Function.rightInverse_surjInv :
∀ {α : Sort u} {β : Sort v} {f : α → β} (hf : Function.Surjective f),
Function.RightInverse (Function.surjInv hf) f
This theorem states that for any sets `α` and `β`, and function `f` that maps `α` to `β`, if `f` is surjective (meaning every element in `β` can be mapped from some element in `α`), then the function `surjInv hf` is a right inverse to `f`. In other words, the composition of `f` and `surjInv hf` (in that order) is the identity function on `β`. In mathematical notation, this would be expressed as `f ∘ (surjInv hf) = id`, where `id` is the identity function. The function `surjInv hf` is defined as the inverse of the surjective function `f`.
More concisely: For any surjective function `f` from set `α` to set `β`, there exists a unique function `g` from `β` to `α` such that `f ∘ g = id_{{\beta}}`.
|
Symmetric.forall_existsUnique_iff'
theorem Symmetric.forall_existsUnique_iff' :
∀ {α : Sort u_1} {r : α → α → Prop},
Symmetric r → ((∀ (a : α), ∃! b, r a b) ↔ ∃ f, Function.Involutive f ∧ r = fun x x_1 => f x = x_1)
This theorem states that for any symmetric relation `r` on some type `α` (that is, a relation for which `x is related to y` implies `y is related to x`), this relation behaves like a function (that is, for each element `a`, there exists a unique element `b` such that `a is related to b`) if and only if it can be expressed as the equality under some function `f` which is involutive (meaning applying `f` twice to any input gives back the original input). In symbolic form, this can be expressed as `∀a, ∃!b, r a b` if and only if `∃f, f(f(x)) = x ∧ r a b = (f a = b)`.
More concisely: A symmetric relation on a type behaves like a function if and only if it can be expressed as the equality under some involutive function.
|
Function.extend_comp
theorem Function.extend_comp :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
Function.Injective f → ∀ (g : α → γ) (e' : β → γ), Function.extend f g e' ∘ f = g
This theorem states that for any three types `α`, `β`, and `γ`, and any function `f` from `α` to `β`, if `f` is injective (meaning that equal outputs imply equal inputs), then for any function `g` from `α` to `γ` and any function `e'` from `β` to `γ`, the composition of the extension of `f`, `g`, and `e'` with `f` equals to `g`. In other words, if we first apply `f` to an input and then apply the extended function, it's as if we directly applied `g`. The theorem ties together function composition, function extension and injective functions in a precise way.
More concisely: If `f: α → β` is injective and `g: α → γ` and `e': β → γ` are functions, then `(g ∘ e') ∘ f = g ∘ (extension f g)`.
|