forall_not_of_not_exists
theorem forall_not_of_not_exists : ∀ {α : Sort u_1} {p : α → Prop}, (¬∃ x, p x) → ∀ (x : α), ¬p x
This theorem, `forall_not_of_not_exists`, is an alias for the forward direction of `not_exists`. It states that for any type `α` and any property `p` that elements of `α` might have, if there is no element of `α` that has property `p` (expressed as `¬∃ x, p x`), then it must be the case that for every element `x` of `α`, `x` does not have property `p` (expressed as `∀ (x : α), ¬p x`). This theorem essentially provides a link between the non-existence of an element with a certain property and the non-possession of that property by every individual element.
More concisely: If there exists no element in a type with a certain property, then that property is void for every element in that type.
|
Classical.exists_not_of_not_forall
theorem Classical.exists_not_of_not_forall : ∀ {α : Sort u_1} {p : α → Prop}, (¬∀ (x : α), p x) → ∃ x, ¬p x
This theorem, `Classical.exists_not_of_not_forall`, is an alias for the forward direction of `Classical.not_forall`. It states that, for any type `α` and any property `p` that elements of `α` might have, if it is not the case that all elements of `α` have property `p`, then there exists some element in `α` that does not have property `p`. This is a basic result in classical logic.
More concisely: If it is not the case that all elements of type `α` have property `p`, then there exists an element in `α` that does not have property `p`.
|
congr_arg
theorem congr_arg : ∀ {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
The Lean 4 theorem `congr_arg` is about congruence in arguments of a function. It states that for any two elements `a₁` and `a₂` in a sort `α`, and any function `f` mapping from `α` to another sort `β`, if `a₁` is equal to `a₂`, then the results of applying `f` to `a₁` and `a₂` are also equal, i.e., `f a₁ = f a₂`. This theorem is notably more potent than initially apparent, as it also permits the use of a lambda expression for `f`, allowing us to prove that some expression involving `a₁` is equal to a corresponding expression involving `a₂`. Tactics like `congr` and `simp` use this theorem internally to apply equalities within subterms.
More concisely: For any function `f` and elements `a₁` and `a₂` in a sort `α`, if `a₁` equals `a₂`, then `f a₁` equals `f a₂`.
|
subsingleton_of_forall_eq
theorem subsingleton_of_forall_eq : ∀ {α : Sort u_1} (x : α), (∀ (y : α), y = x) → Subsingleton α
This theorem states that for any type (or sort) `α` and given an element `x` of this type, if all elements `y` in `α` are equal to `x`, then `α` is a subsingleton. In mathematical terms, a subsingleton is a set (or type in Lean 4) that has at most one element. Here, the theorem is stating that if every element of a type is identical (specifically, identical to `x`), then the type must be a subsingleton, as it contains at most one distinct element.
More concisely: If every element of a type `α` is equal to a given element `x`, then `α` is a subsingleton (has at most one element).
|
funext₂
theorem funext₂ :
∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f g : (a : α) → (b : β a) → γ a b},
(∀ (a : α) (b : β a), f a b = g a b) → f = g
This theorem, `funext₂`, is a generalized statement of function extensionality in Lean 4. It states that for all types `α`, `β` (which is dependent on `α`), and `γ` (which is dependent on both `α` and `β`), and for all functions `f` and `g` that map a pair of values from `α` and `β` to `γ`, if `f` and `g` are pointwise equal (i.e., for all `a` from `α` and `b` from `β`, `f a b` equals `g a b`), then `f` is identical to `g`. In simpler terms, two functions are the same if they give the same output for every input.
More concisely: For all types `α`, `β`, and dependent types `γ`, if two functions `f` and `g` from `α × β` to `γ` agree on all inputs, then they are equal.
|
congr_fun
theorem congr_fun : ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
The theorem `congr_fun` expresses the idea of congruence in function application. It states that for any two functions `f` and `g` from a sort `α` to a sort `β` that depends on `α`, if `f` and `g` are equal (i.e., `f = g`), then applying `f` and `g` to the same element `a` in `α` will also give equal results (i.e., `f a = g a`). This is a fundamental property of function application in Mathematics.
More concisely: If `f` and `g` are equal functions from sort `α` to sort `β`, then `f(a) = g(a)` for all `a` in `α`.
|
congr_fun₃
theorem congr_fun₃ :
∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4}
{f g : (a : α) → (b : β a) → (c : γ a b) → δ a b c}, f = g → ∀ (a : α) (b : β a) (c : γ a b), f a b c = g a b c
The theorem `congr_fun₃` states that for any four dependent types `α`, `β`, `γ`, and `δ`, and two functions `f` and `g` that map an element of `α`, an element of `β` dependent on `α`, and an element of `γ` dependent on `α` and `β`, to an element of `δ` dependent on `α`, `β`, and `γ`, if `f` equals `g`, then for any element `a` of `α`, an element `b` of `β` dependent on `a`, and an element `c` of `γ` dependent on `a` and `b`, `f a b c` equals `g a b c`. In short, it asserts the equality of two functions under the assumption that they are identical.
More concisely: Given functions `f` and `g` from `α × β(α) × γ(α, β)` to `δ(α, β, γ)`, if `f = g`, then for all `a : α`, `b : β(a)`, and `c : γ(a, b)`, `f a b c = g a b c`.
|
heq_iff_eq
theorem heq_iff_eq : ∀ {α : Sort u_1} {a b : α}, HEq a b ↔ a = b
This theorem states that for any type `α` and any two elements `a` and `b` of this type, the higher-level equality (`HEq`) between `a` and `b` is equivalent to the standard equality (`=`) between `a` and `b`. In other words, the higher-order equality is the same as the standard equality for elements of the same type in Lean 4.
More concisely: For any type `α` and any `a, b : α`, the higher-level equality `α.HEq a b` is equivalent to the standard equality `a = b`.
|
Decidable.exists_not_of_not_forall
theorem Decidable.exists_not_of_not_forall :
∀ {α : Sort u_1} {p : α → Prop} [inst : Decidable (∃ x, ¬p x)] [inst : (x : α) → Decidable (p x)],
(¬∀ (x : α), p x) → ∃ x, ¬p x
The theorem `Decidable.exists_not_of_not_forall` is an alias of the forward direction of `Decidable.not_forall`. It states that for any type `α` and any predicate `p` on `α`, if it is not the case that `p` holds for all elements of `α`, then there exists an element of `α` for which `p` does not hold. The decidability of the existence of such an element, as well as the decidability of `p` for each `x` in `α`, are assumed.
More concisely: If `p` is a decidable predicate on a type `α` such that there exists no element `x` in `α` with `p(x)` holding for all `x` in `α`, then there exists an element `x` in `α` with `p(x)` failing.
|
congrArg₂
theorem congrArg₂ :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) {x x' : α} {y y' : β},
x = x' → y = y' → f x y = f x' y'
The theorem `congrArg₂` states that for all types `α`, `β`, and `γ`, and a function `f` from `α` and `β` to `γ`, if `x` equals `x'` and `y` equals `y'`, then applying `f` to `x` and `y` is the same as applying `f` to `x'` and `y'`. In other words, if two pairs of inputs to a two-argument function are equal respectively, then the outputs of the function applied to these two pairs are also equal.
More concisely: For all types α, β, γ and functions f : α → β → γ, if x = x' and y = y', then f x y = f x' y'.
|
eq_rec_constant
theorem eq_rec_constant : ∀ {α : Sort u_1} {a a' : α} {β : Sort u_2} (y : β) (h : a = a'), h ▸ y = y
This theorem, named `eq_rec_constant`, states that for any types `α` and `β`, any elements `a` and `a'` of type `α`, and any element `y` of type `β`, if `a` equals `a'` (denoted as `a = a'`), then substituting `a'` for `a` in `y` (denoted as `h ▸ y`) results in `y` itself. In other words, the operation of substituting an equal object into another object doesn't change the latter object. This theorem holds in a general context, with `α` and `β` being of any sort.
More concisely: For all types `α` and `β`, and elements `a : α`, `a' : α`, and `y : β`, if `a = a'`, then `h ▸ y` equals `y`.
|
heq_of_cast_eq
theorem heq_of_cast_eq : ∀ {α β : Sort u_1} {a : α} {a' : β} (e : α = β), cast e a = a' → HEq a a'
This theorem, `heq_of_cast_eq`, states that for any two types `α` and `β` and any two values `a` of type `α` and `a'` of type `β`, if `α` equals `β` (denoted as `e : α = β`) and the value `a` becomes `a'` after being cast from type `α` to `β` (denoted as `cast e a = a'`), then `a` and `a'` are heterogeneously equal, represented as `HEq a a'`. In other words, if we can cast an element of one type to an element of another type, and these types turn out to be the same, then the original and the casted element are heterogeneously equal. This theorem is involved in the area of type theory in mathematics.
More concisely: If `α = β` and `cast : α → β` is a type-preserving function with `cast (x : α) = a'`, then `x` and `a'` are heterogeneously equal, denoted as `HEq x a'`.
|
congr_arg₂
theorem congr_arg₂ :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) {x x' : α} {y y' : β},
x = x' → y = y' → f x y = f x' y'
This theorem, known as `congr_arg₂`, states that for any three types α, β, and γ and a function `f` from α and β to γ, if `x` and `x'` are equal elements of type α and `y` and `y'` are equal elements of type β, then the result of applying `f` to `x` and `y` is equal to the result of applying `f` to `x'` and `y'`. This is essentially a generalization of the congruence property in mathematics, extended to a function of two variables.
More concisely: For all types α, β, γ and functions f : α → β → γ, if x = x' in α and y = y' in β, then f x y = f x' y' in γ.
|
ne_of_apply_ne
theorem ne_of_apply_ne : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) {x y : α}, f x ≠ f y → x ≠ y
This theorem, `ne_of_apply_ne`, states that for any two types `α` and `β`, and a function `f` from `α` to `β`, if the function `f` applied to two values `x` and `y` of type `α` gives different results (i.e., `f x` is not equal to `f y`), then `x` is not equal to `y`. In other words, if the function outputs are different for two inputs, then the inputs themselves must also be different.
More concisely: If `f : α → β` is a function and `x` and `y` are in `α` with `f x ≠ f y`, then `x ≠ y`.
|
not_exists_of_forall_not
theorem not_exists_of_forall_not : ∀ {α : Sort u_1} {p : α → Prop}, (∀ (x : α), ¬p x) → ¬∃ x, p x
This theorem, named `not_exists_of_forall_not`, is an alias of the reverse direction of `not_exists`. It states that for any type `α` and any property `p` that applies to elements of the type `α`, if it is true that for all `x` of type `α` the property `p` does not hold (`¬p x`), then it follows that there does not exist any `x` of type `α` for which the property `p` holds (`¬∃ x, p x`).
More concisely: If for all x in type α, property p(x) is false, then there exists no x in α such that p(x) holds.
|
cast_eq_iff_heq
theorem cast_eq_iff_heq : ∀ {a a_1 : Sort u_1} {e : a = a_1} {a_2 : a} {a' : a_1}, cast e a_2 = a' ↔ HEq a_2 a' := by
sorry
This theorem states that for any two sorts `a` and `a_1` of the same universe `u_1`, and given `e` is an equality between `a` and `a_1`, an element `a_2` of `a` and an element `a'` of `a_1`, then the casting of `a_2` to `a_1` using `e` is equal to `a'` if and only if `a_2` and `a'` are heterogeneously equal. "Heterogeneously equal" (HEq) means that `a_2` and `a'` are equal even if they are of different types, as long as their types are themselves equal.
More concisely: For any sorts `a` and `a_1` of the same universe `u_1`, and given `e : a = a_1`, `a_2 : a`, and `a' : a_1`, `e.cast a_2 = a'` if and only if `a_2` and `a'` are heterogeneously equal.
|
ne_of_mem_of_not_mem
theorem ne_of_mem_of_not_mem :
∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {s : β} {a b : α}, a ∈ s → b ∉ s → a ≠ b
This theorem states that for any types `α` and `β` where `α` has a membership relation with `β`, given an instance `s` of `β` and two instances `a` and `b` of `α`, if `a` is a member of `s` and `b` is not a member of `s`, then `a` is not equal to `b`. In mathematical terms, if $a$ belongs to a set $s$ and $b$ does not belong to the same set, then $a$ is not equal to $b$.
More concisely: If $a$ is an element of set $s$ and $b$ is not an element of $s$, then $a$ is not equal to $b$.
|
Eq.congr
theorem Eq.congr : ∀ {α : Sort u_1} {x₁ y₁ x₂ y₂ : α}, x₁ = y₁ → x₂ = y₂ → (x₁ = x₂ ↔ y₁ = y₂)
The theorem `Eq.congr` states that for any type `α`, given four elements of this type (`x₁`, `y₁`, `x₂`, `y₂`), if `x₁` is equal to `y₁` and `x₂` is equal to `y₂`, then `x₁` equals `x₂` if and only if `y₁` equals `y₂`. Essentially, this theorem is about the transitivity of equality: if two pairs of elements are each equal within their pair, then equality between any element from the first pair and any element from the second pair is equivalent to equality between the remaining elements.
More concisely: If `x₁ = y₁` and `x₂ = y₂`, then `x₁ = x₂`.
|
Eq.congr_left
theorem Eq.congr_left : ∀ {α : Sort u_1} {x y z : α}, x = y → (x = z ↔ y = z)
This theorem, `Eq.congr_left`, states that for any type `α` and any elements `x`, `y`, and `z` of type `α`, if `x` is equal to `y`, then `x` being equal to `z` is logically equivalent to `y` being equal to `z`. Essentially, it says that if we have two equivalent elements, we can interchange them in any equality relation without affecting the truth value of the relation.
More concisely: If `x = y` then `x = z` if and only if `y = z`.
|
Function.funext_iff
theorem Function.funext_iff :
∀ {α : Sort u_1} {β : α → Sort u} {f₁ f₂ : (x : α) → β x}, f₁ = f₂ ↔ ∀ (a : α), f₁ a = f₂ a
This theorem, referred to as `Function.funext_iff`, states that for any two functions `f₁` and `f₂` that map elements from a certain type `α` to another dependent type `β`, these functions are considered equal if and only if they produce the same result for every element in `α`. This theorem is a formalization of the principle of function extensionality in the Lean theorem prover. This principle is fundamental in mathematics, expressing the idea that two functions are the same if they give the same output for every input.
More concisely: Two functions from type `α` to a dependent type `β` are equal if and only if they agree on all elements of `α`.
|
congr_fun₂
theorem congr_fun₂ :
∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f g : (a : α) → (b : β a) → γ a b},
f = g → ∀ (a : α) (b : β a), f a b = g a b
This theorem, referred to as an alias of `congrFun₂`, states that for any two functions `f` and `g` that map an element `a` of type `α` and an element `b` of a dependent type `β a` to an element of a dependent type `γ a b`, if `f` and `g` are equal, then for any specific `a` and `b` (where `b` is of type `β a`), `f a b` is equal to `g a b`. Essentially, it asserts that if two functions are equal, their outcomes are equal for each possible pair of input.
More concisely: If two functions `f` and `g` from `α × β (α)` to `γ (α) (β (α))` are equal, then for all `a : α` and `b : β a`, `f a b` is equal to `g a b`.
|