Prod.mk.inj
theorem Prod.mk.inj :
∀ {α : Type u} {β : Type v} {fst : α} {snd : β} {fst_1 : α} {snd_1 : β},
(fst, snd) = (fst_1, snd_1) → fst = fst_1 ∧ snd = snd_1
This theorem, `Prod.mk.inj`, states that for any two pairs of types `(α, β)` and `(α, β)`, if a pair `(fst, snd)` is equal to another pair `(fst_1, snd_1)`, then the first element `fst` is equal to the first element `fst_1` of the second pair and the second element `snd` is equal to the second element `snd_1` of the second pair. In other words, it asserts that if two pairs are equal, their corresponding elements are also equal.
More concisely: Given pairs `(α, β)` and `(α', β')`, if `(α, β)` = `(α', β')`, then `α` = `α'` and `β` = `β'`.
|
HEq.symm
theorem HEq.symm : ∀ {α β : Sort u} {a : α} {b : β}, HEq a b → HEq b a
This theorem states that heterogeneous equality (`HEq`) in Lean 4 is symmetrical. Specifically, for any two types `α` and `β` in a given sort `u`, and any two values `a` of type `α` and `b` of type `β`, if `a` is heterogeneously equal to `b`, then `b` is also heterogeneously equal to `a`. Heterogeneous equality allows comparison of values of different types, contrasting with homogeneous equality which requires both values to be of the same type.
More concisely: For all types `α` and `β` in sort `u` and values `a : α` and `b : β`, if `a =_|_ b` then `b =_|_ a`, where `=_|_` denotes heterogeneous equality.
|
Eq.to_iff
theorem Eq.to_iff : ∀ {a b : Prop}, a = b → (a ↔ b)
This theorem, `Eq.to_iff`, states that for any two propositions `a` and `b`, if `a` is equal to `b`, then `a` is logically equivalent to `b`. In other words, if two propositions are the same (`a = b`), then they imply each other (`a ↔ b`). It's a fundamental connection between the concepts of equality and logical equivalence in propositional logic.
More concisely: If two propositions are equal, then they are logically equivalent. (a = b ↔ a ↔ b)
|
iff_iff_implies_and_implies
theorem iff_iff_implies_and_implies : ∀ (a b : Prop), (a ↔ b) ↔ (a → b) ∧ (b → a)
This theorem states that for any two propositional variables `a` and `b`, the biconditional statement `a ↔ b` (which reads "a if and only if b") is equivalent to the conjunction of two implications: `a → b` and `b → a` (which reads "a implies b and b implies a"). Essentially, it is asserting that the "if and only if" relationship between two propositions can be expressed as a pair of mutual implications.
More concisely: For any propositional variables `a` and `b`, the biconditional `a ↔ b` is logically equivalent to the conjunction of `a → b` and `b → a`.
|
Decidable.em
theorem Decidable.em : ∀ (p : Prop) [inst : Decidable p], p ∨ ¬p
This theorem, `Decidable.em`, states that for any proposition `p`, given that `p` is decidable (i.e., we can definitively assert whether `p` is true or false), then either `p` is true or `p` is not true. In mathematical terms, this is an instantiation of the law of excluded middle, which asserts that for any proposition, either that proposition or its negation must be true.
More concisely: If a proposition `p` is decidable, then `p` or its negation `~p` is true.
|
Iff.subst
theorem Iff.subst : ∀ {a b : Prop} {p : Prop → Prop}, (a ↔ b) → p a → p b
This theorem, `Iff.subst`, states that given two propositions `a` and `b`, and a property `p` that applies to propositions, if `a` is equivalent to `b` (represented by `a ↔ b`), then the property `p` holding for `a` implies that the same property holds for `b`. In other words, we can substitute `b` for `a` in the property `p` if `a` and `b` are logically equivalent.
More concisely: If `a` is equivalent to `b`, then `p(a)` implies `p(b)` for any property `p`.
|
Not.imp
theorem Not.imp : ∀ {a b : Prop}, ¬b → (a → b) → ¬a
This theorem states that for any two propositions `a` and `b`, if `b` is not true (denoted by `¬b`), and if `a` implies `b` (denoted by `a → b`), then `a` is also not true (denoted by `¬a`). This is a fundamental result in logic, expressing the idea that if a proposition's truth implies the truth of a falsehood, then the original proposition itself must be false.
More concisely: If `a` implies `b` and `¬b` holds, then `¬a` holds. (This is known as the contrapositive of the implication "if `a`, then `b`," and is logically equivalent to it.)
|
Option.some.injEq
theorem Option.some.injEq : ∀ {α : Type u} (val val_1 : α), (some val = some val_1) = (val = val_1)
This theorem, `Option.some.injEq`, states that for any type `α` and for any two values `val` and `val_1` of this type, the equality of `some val` and `some val_1` is equivalent to the equality of `val` and `val_1`. In other words, in the `Option` type constructor, `some` is injective: two `some` values are equal if and only if the values they contain are equal.
More concisely: For any type `α`, the function `some : α -> Option α` is an injection. That is, for all `val` and `val_1` of type `α`, `some val = some val_1` if and only if `val = val_1`.
|
Subtype.mk.injEq
theorem Subtype.mk.injEq :
∀ {α : Sort u} {p : α → Prop} (val : α) (property : p val) (val_1 : α) (property_1 : p val_1),
(⟨val, property⟩ = ⟨val_1, property_1⟩) = (val = val_1)
This theorem, named `Subtype.mk.injEq`, states that for any type `α` and any property `p` pertaining to `α`, two subtypes created with the same value and property are equal if and only if their values are equal. Here, a subtype is created by providing a value of type `α` and a proof that the value satisfies property `p` (`{ val := val, property := property }`). The theorem formalizes the idea that the equality of these subtypes hinges purely on the equality of their contained values, irrespective of the properties associated with them.
More concisely: For any type `α` and property `p`, two subtypes `{ val := a, property := p }` and `{ val := b, property := p }` of `α` are equal if and only if `a = b`.
|
Quotient.inductionOn₂
theorem Quotient.inductionOn₂ :
∀ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Prop}
(q₁ : Quotient s₁) (q₂ : Quotient s₂), (∀ (a : α) (b : β), motive ⟦a⟧ ⟦b⟧) → motive q₁ q₂
The theorem `Quotient.inductionOn₂` states that for any given sorts `α` and `β`, and for any given setoids `s₁` and `s₂` on these sorts, if we have a property `motive` that relates an element of the quotient set of `s₁` to an element of the quotient set of `s₂`, then if this property holds for all pairs of equivalence classes of `s₁` and `s₂`, it will also hold for any two given equivalence classes `q₁` and `q₂` of `s₁` and `s₂` respectively. In other words, the theorem allows us to perform an induction on pairs of elements from two quotient sets, under the assumption that our inductive property is preserved by the equivalence relations defining the quotient sets.
More concisely: If `motive` is a relation between equivalence classes of two setoids `s₁` and `s₂`, and `motive` holds for all pairs of equivalence classes if and only if it holds for `q₁` and `q₂`, then `motive` holds for the equivalence classes `q₁` and `q₂` of `s₁` and `s₂` respectively.
|
Not.intro
theorem Not.intro : ∀ {a : Prop}, (a → False) → ¬a
This theorem, `Not.intro`, states that for any proposition `a`, if we can show that `a` implies `False`, then we can conclude that `a` is not true, or in other words, `¬a` holds. This is a formalization of the principle of proof by contradiction in logic, where we assume a proposition and derive a contradiction to show that the original proposition cannot be true.
More concisely: If `a` implies `False`, then `¬a` holds. (Or, if derived contradiction from `a`, then `a` is false.)
|
funext
theorem funext : ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
The theorem `funext` is a statement of **Function Extensionality** in Lean. It asserts that if two functions, `f` and `g`, of a dependent type `β` indexed over a sort `α`, provide equal outcomes for every possible value of `α`, then the functions `f` and `g` themselves are considered equal. Formally, it is expressed as `(∀ x, f x = g x) → f = g`.
This concept is known as "extensionality", as it allows us to establish equality between two entities based on their properties. It's important to note that this is often assumed as an axiom in dependent type theory systems, because it is not provable using only the core logic. However, in Lean's type theory, this can be derived from the existence of quotient types.
More concisely: If two functions `f` and `g` of type `β -> α` have the same output for all `α`, then `f` and `g` are equal.
|
imp_congr_right
theorem imp_congr_right : ∀ {a b c : Prop}, (a → (b ↔ c)) → (a → b ↔ a → c)
This theorem states that, for any three propositions `a`, `b`, and `c`, if we assume that whenever `a` holds, `b` is equivalent to `c`, then we can conclude that `a` implies `b` is equivalent to `a` implying `c`. In other words, if whether `a` implies `b` depends solely on whether `a` also implies `c`, then the two implications are equivalent under the assumption of `a`. This theorem is a statement about the transitivity of logical implications in propositional logic.
More concisely: If `a` implies `b` is equivalent to `c` whenever `a` holds, then `a` implies `b` is equivalent to `a` implies `c`.
|
Subtype.eq
theorem Subtype.eq : ∀ {α : Type u} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
This theorem, named `Subtype.eq`, states that for any type `α` and any predicate `p` applying to `α`, given two subtypes `a1` and `a2` (i.e., elements of type `α` that satisfy predicate `p`), if the underlying elements of `a1` and `a2` (obtained by applying the coercion function `↑` to `a1` and `a2`) are equal, then `a1` and `a2` themselves are equal. Essentially, it says that if two subtypes have the same underlying value, they are the same subtype.
More concisely: If two subtypes of a type with a given predicate have equal underlying elements, then they are equal as subtypes.
|
Iff.refl
theorem Iff.refl : ∀ (a : Prop), a ↔ a
This theorem, `Iff.refl`, asserts that for any proposition `a`, `a` is logically equivalent to itself. In other words, it establishes the reflexivity of logical equivalence. For any proposition, it is always true that the proposition implies itself and is implied by itself. This is a fundamental concept in logic.
More concisely: For all propositions `a`, `a` is logically equivalent to itself.
|
Function.comp_def
theorem Function.comp_def :
∀ {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} (f : β → δ) (g : α → β), f ∘ g = fun x => f (g x)
The theorem `Function.comp_def` states that for all types `α`, `β`, and `δ`, and any two functions `f` from `β` to `δ` and `g` from `α` to `β`, the composition of `f` and `g` (denoted as `f ∘ g`) is the same as the function that takes an input `x` of type `α`, applies the function `g` to `x`, and then applies the function `f` to the result. In mathematical terms, this expresses the definition of function composition: `(f ∘ g)(x) = f(g(x))`.
More concisely: The `Function.comp_def` theorem in Lean 4 asserts that for all types `α`, `β`, and `δ`, and functions `f : β → δ` and `g : α → β`, `f ∘ g` is equal to the function that maps `x` in `α` to `f(g(x))`.
|
Setoid.refl
theorem Setoid.refl : ∀ {α : Sort u} [inst : Setoid α] (a : α), a ≈ a
This theorem states that, for any type 'α' equipped with a Setoid structure (which provides an equivalence relation), every element 'a' of type 'α' is equivalent to itself. In mathematical terms, it proves the reflexivity property of the equivalence relation (≈) in the context of setoids: for all 'a' in 'α', a ≈ a. This is a fundamental property of any equivalence relation in mathematics.
More concisely: For any setoid type 'α' and its equivalence relation '≈', every element 'a' in 'α' is equivalent to itself, i.e., a ≈ a.
|
nonempty_of_exists
theorem nonempty_of_exists : ∀ {α : Sort u} {p : α → Prop}, (∃ x, p x) → Nonempty α
This theorem states that for any type `α` and any property `p` that applies to elements of `α`, if there exists an element `x` of `α` that satisfies property `p`, then `α` is nonempty. In more mathematical terms, given any set `α` and any predicate `p : α → Prop`, if there exists an `x` in `α` such that `p(x)` holds true, then set `α` must be nonempty.
More concisely: If a set `α` has an element `x` satisfying a property `p : α → Prop`, then `α` is nonempty.
|
Antisymm.antisymm
theorem Antisymm.antisymm : ∀ {α : Sort u} {r : α → α → Prop} [self : Antisymm r] {a b : α}, r a b → r b a → a = b := by
sorry
This theorem states that for any type `α` and any relation `r` defined on `α`, if `r` is antisymmetric, then for any two elements `a` and `b` of type `α`, if `a` is related to `b` and `b` is related to `a` by `r`, then `a` and `b` must be equal. In other words, in an antisymmetric relation, if `a` and `b` are related in both directions, they must be the same element.
More concisely: In an antisymmetric relation, if `a` is related to `b` and `b` is related to `a`, then `a` equals `b`.
|
iff_true_right
theorem iff_true_right : ∀ {a b : Prop}, a → ((b ↔ a) ↔ b)
This theorem, `iff_true_right`, states that for any two propositions `a` and `b`, if `a` is true, then `b` is equivalent to `a` if and only if `b` is true. In simpler terms, if we know `a` is true, then the statement "`b` is equivalent to `a`" and the statement "`b` is true" are the same.
More concisely: For all propositions `a` and `b`, `a` implies `a <> b <> false` if and only if `b` is true. (Here, `<>` denotes propositional equivalence.)
|
le_of_eq_of_le
theorem le_of_eq_of_le : ∀ {α : Type u} {a b c : α} [inst : LE α], a = b → b ≤ c → a ≤ c
This theorem, named `le_of_eq_of_le`, states that for any type `α` that has a less than or equal to (`≤`) operation, if a certain element `a` is equal to another element `b`, and `b` is less than or equal to a third element `c`, then it must be the case that `a` is also less than or equal to `c`. In other words, it asserts the transitivity of the less than or equal to relation after an equality substitution. This holds for all elements `a`, `b`, `c` of any type `α` with a `≤` relation.
More concisely: If `a ≤ b` and `b = c`, then `a ≤ c`.
|
Iff.rfl
theorem Iff.rfl : ∀ {a : Prop}, a ↔ a
This theorem, `Iff.rfl`, states that for any proposition `a`, `a` is logically equivalent to itself. In other words, it's a statement of reflexivity for logical equivalence in propositional logic. In mathematical terms, for any propositional variable `a`, `a ↔ a` is always true.
More concisely: For all propositions `a`, `a` is logically equivalent to itself (`a ↔ a` is true).
|
Quotient.exact
theorem Quotient.exact : ∀ {α : Sort u} {s : Setoid α} {a b : α}, ⟦a⟧ = ⟦b⟧ → a ≈ b
The theorem `Quotient.exact` states that for any type `α` and a given equivalence relation `s` on `α`, if the equivalence classes of two elements `a` and `b` from `α` are the same (i.e., `⟦a⟧ = ⟦b⟧`), then `a` and `b` are equivalent under the relation `s` (i.e., `a ≈ b`). In the context of set theory, this theorem asserts that two elements belong to the same equivalence class if and only if they are equivalent under the defining relation of that class.
More concisely: For any equivalence relation `s` on type `α`, if `⟦a⟧ = ⟦b�ре�` then `a ≈ b`.
|
proof_irrel
theorem proof_irrel : ∀ {a : Prop} (h₁ h₂ : a), h₁ = h₂
This theorem, `proof_irrel`, states that for any proposition `a`, if there are two proofs `h1` and `h2` of `a`, then `h1` is equal to `h2`. This principle is known as proof irrelevance, and it asserts that two proofs of the same proposition are always identical, meaning there is essentially only one unique proof for a given proposition.
More concisely: If two proofs exist for a proposition, then they are equal. (Proof irrelevance)
|
Prod.mk.injEq
theorem Prod.mk.injEq :
∀ {α : Type u} {β : Type v} (fst : α) (snd : β) (fst_1 : α) (snd_1 : β),
((fst, snd) = (fst_1, snd_1)) = (fst = fst_1 ∧ snd = snd_1)
This theorem, `Prod.mk.injEq`, states that for any two pairs of types `(α, β)` and `(α_1, β_1)`, the equality of these two pairs is equivalent to the equality of both their corresponding first and second elements. In other words, two pairs are equal if and only if their corresponding elements are equal. This theorem holds for any types `α` and `β`, and any elements `fst, fst_1` of type `α` and `snd, snd_1` of type `β`.
More concisely: For any types `α` and `β` and elements `(a, b) : Type ↔ (a' : α) × (b' : β)`, `(a = a') ∧ (b = b')` if and only if `(a, b) = (a', b')`.
|
Quotient.ind
theorem Quotient.ind :
∀ {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop},
(∀ (a : α), motive ⟦a⟧) → ∀ (q : Quotient s), motive q
This theorem serves as the counterpart to `Quot.ind` for the `Quotient` type. It asserts that for any type `α`, any setoid `s` on `α`, and any property `motive` that you might want to prove about elements of the quotient type `Quotient s`, if you have a proof that `motive` holds for any element `a : α` (under the equivalence class ⟦a⟧), then `motive` holds for all elements `q : Quotient s`. In mathematical terms, this can be interpreted as saying that properties of representatives of an equivalence class can be lifted to the entire equivalence class in the quotient set.
More concisely: If `motive` is a property that preserves the equivalence relation `s` on `α`, then `motive` holds for all elements of the quotient type `Quotient s`.
|
eq_self_iff_true
theorem eq_self_iff_true : ∀ {α : Sort u_1} (a : α), a = a ↔ True
This theorem, `eq_self_iff_true`, states that for any sort `α` and any instance `a` of `α`, the equality of `a` to itself is equivalent to the truth value `True`. In other words, an element is always equal to itself, and this self-equality can be replaced with `True` in logical expressions. This is a fundamental property of equality in mathematics, often known as the Reflexivity of Equality.
More concisely: For all types α and elements a : α, a = a if and only if True. (Reflexivity of Equality)
|
dif_pos
theorem dif_pos : ∀ {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : c → α} {e : ¬c → α}, dite c t e = t hc := by
sorry
The theorem `dif_pos` states that for any proposition `c`, given that it is decidable and true (`hc : c`), and given two functions `t : c → α` and `e : ¬c → α`, the expression `dite c t e` (if `c` then `t` else `e`) will equal `t hc`. In other words, if the condition `c` is true, then the if-then-else expression will evaluate to the function `t` applied to the proof of `c`.
More concisely: If `c` is a decidable and true proposition, then `dite c t e` equals `t (proof of c)`.
|
Sum.inr.inj
theorem Sum.inr.inj : ∀ {α : Type u} {β : Type v} {val val_1 : β}, Sum.inr val = Sum.inr val_1 → val = val_1
This theorem, `Sum.inr.inj`, states that for any types `α` and `β`, and for any two values `val` and `val_1` of type `β`, if `Sum.inr val` is equal to `Sum.inr val_1`, then `val` is equal to `val_1`. In other words, the `inr` function of the `Sum` type is injective (or one-to-one), meaning that equal outputs can only come from equal inputs.
More concisely: For all types α and β, the injective function `inr : β -> Sum β α` holds that `inr a = inr a'` implies `a = a'`.
|
Subtype.mk.inj
theorem Subtype.mk.inj :
∀ {α : Sort u} {p : α → Prop} {val : α} {property : p val} {val_1 : α} {property_1 : p val_1},
⟨val, property⟩ = ⟨val_1, property_1⟩ → val = val_1
The theorem `Subtype.mk.inj` states that for any sort `α`, any predicate `p` on `α`, and any two values `val` and `val_1` of type `α` that satisfy the predicate `p`, if two subtypes created with these pairs of values and proofs are equal, then the original values `val` and `val_1` must also be equal. In other words, the constructor for a subtype is injective, meaning it produces a unique subtype for each unique pair of a value and a proof that the value satisfies the predicate.
More concisely: If `α` is a sort, `p` is a predicate on `α`, and `val` and `val_1` are values of type `α` satisfying `p`, then the equality of their corresponding subtypes `{x : α | p x} with (val, rfl) = {x : α | p x} with (val_1, rfl)` implies `val = val_1`.
|
And.comm
theorem And.comm : ∀ {a b : Prop}, a ∧ b ↔ b ∧ a
This theorem, `And.comm`, states that for any two propositions `a` and `b`, the logical conjunction `a ∧ b` (a AND b) is logically equivalent to `b ∧ a` (b AND a). This represents the commutative property of logical conjunction in propositional logic.
More concisely: For all propositions `a` and `b`, `a ∧ b` is equivalent to `b ∧ a` in propositional logic.
|
Subsingleton.allEq
theorem Subsingleton.allEq : ∀ {α : Sort u} [self : Subsingleton α] (a b : α), a = b
This theorem states that in the context of a subsingleton, any two elements are equal. Here, a subsingleton is specified by `α : Sort u` with a provided instance of the Subsingleton property for `α`. The theorem then takes any two elements `a` and `b` of this subsingleton and states that `a` and `b` are equal. In a more mathematical language, this theorem can be articulated as: "For all `α` of some sort `u` that is a subsingleton, for all elements `a` and `b` of `α`, `a` equals `b`." This captures the defining property of a subsingleton, which is a type with at most one element.
More concisely: In a subsingleton type `α` with the Subsingleton property, any two elements are equal.
|
eq_comm
theorem eq_comm : ∀ {α : Sort u_1} {a b : α}, a = b ↔ b = a
This theorem is named `eq_comm`, which stands for "equality is commutative". It states that for any sort `α` and any two elements `a` and `b` of `α`, `a` is equal to `b` if and only if `b` is equal to `a`. In mathematical terms, this theorem asserts the commutativity of equality, i.e., if $a = b$, then $b = a$, for any elements $a$ and $b$ of any sort $α$. This is a fundamental property of equality in mathematics.
More concisely: For all sorts `α` and elements `a`, `b` of `α`, `a = b` if and only if `b = a`.
|
Nat.succ.inj
theorem Nat.succ.inj : ∀ {m n : ℕ}, m.succ = n.succ → m = n
This theorem, `Nat.succ.inj`, states that for any two natural numbers `n` and `n_1`, if the successor (the next natural number) of `n` is equal to the successor of `n_1`, then `n` must be equal to `n_1`. In other words, if `n+1` equals `n_1+1`, then `n` equals `n_1`. This is an application of the principle of injectivity of the successor function in the natural numbers.
More concisely: If for natural numbers `n` and `n_1`, `n+1 = n_1+1`, then `n = n_1`.
|
ge_iff_le
theorem ge_iff_le : ∀ {α : Type u} [inst : LE α] {x y : α}, x ≥ y ↔ y ≤ x
This theorem, `ge_iff_le`, states that for all types `α` equipped with a less than or equal to (`≤`) ordering, and for any two elements `x` and `y` of type `α`, `x` is greater than or equal to `y` if and only if `y` is less than or equal to `x`. This is a universal property of ordered sets, and is essentially a restatement of the definition of "greater than or equal to" in terms of "less than or equal to".
More concisely: For all types `α` with a `≤` ordering, `x ≤ y` if and only if `y ≤ x`.
|
Sum.inl.injEq
theorem Sum.inl.injEq : ∀ {α : Type u} {β : Type v} (val val_1 : α), (Sum.inl val = Sum.inl val_1) = (val = val_1) := by
sorry
This theorem, `Sum.inl.injEq`, states that for any types `α` and `β`, and any two values `val` and `val_1` of type `α`, the equality of `Sum.inl val` and `Sum.inl val_1` is equivalent to the equality of `val` and `val_1`. In other words, wrapping two values of type `α` into the left component of the sum type does not change their equality status.
More concisely: For all types `α` and values `val` and `val_1` of type `α`, `Sum.inl val = Sum.inl val_1` if and only if `val = val_1`.
|
Exists.elim
theorem Exists.elim : ∀ {α : Sort u} {p : α → Prop} {b : Prop}, (∃ x, p x) → (∀ (a : α), p a → b) → b
This theorem, `Exists.elim`, states that for any sort `α`, any predicate `p` on `α`, and any proposition `b`, if there exists an element in `α` that satisfies `p`, and assuming that for any element in `α`, if it satisfies `p` then `b` is true, then `b` must be true. It essentially says that if `b` follows from a property that is satisfied by at least one element, then `b` is true. This is a form of existential elimination in logical reasoning.
More concisely: If there exists an `α` such that `p(α)` holds and for all `x`, if `p(x)` then `b`, then `b` holds.
|
iff_of_true
theorem iff_of_true : ∀ {a b : Prop}, a → b → (a ↔ b)
This theorem, `iff_of_true`, states that for all propositions `a` and `b`, if `a` is true and `b` is true, then `a` is equivalent to `b`. In other words, if we know that both `a` and `b` are true, we can conclude that `a` if and only if `b`. This is a basic result in propositional logic.
More concisely: For all propositions `a` and `b`, `(a ∧ b)` is logically equivalent to `(a ≤fFAULT b ∧ b ≤fFAULT a)`. (Note: Lean uses the symbols `∧` for logical and, `≤fFAULT` for logical equivalence.)
|
imp_congr
theorem imp_congr : ∀ {a b c d : Prop}, (a ↔ c) → (b ↔ d) → (a → b ↔ c → d)
This theorem, `imp_congr`, states that for any four propositions `a`, `b`, `c`, and `d`, if `a` is logically equivalent to `c` and `b` is logically equivalent to `d`, then the implication `a` implies `b` is logically equivalent to the implication `c` implies `d`. In other words, if we have two pairs of equivalent propositions, the implications between the propositions within each pair are also equivalent.
More concisely: If `a` is logically equivalent to `c` and `b` is logically equivalent to `d`, then the implication `a → b` is logically equivalent to `c → d`.
|
HEq.trans
theorem HEq.trans : ∀ {α β φ : Sort u} {a : α} {b : β} {c : φ}, HEq a b → HEq b c → HEq a c
This theorem, named `HEq.trans`, establishes the transitivity of heterogeneous equality (`HEq`) in Lean. Given three types `α`, `β`, and `φ`, and three objects `a : α`, `b : β`, and `c : φ`, if `a` is heterogeneously equal to `b` and `b` is heterogeneously equal to `c`, then `a` is heterogeneously equal to `c`. Heterogeneous equality allows for the comparison of objects that potentially could be of different types.
More concisely: If `a` is heterogeneously equal to `b` and `b` is heterogeneously equal to `c`, then `a` is heterogeneously equal to `c`. (In other words, `HEq.trans (HEq a b) (HEq b c)` holds in Lean.)
|
Ne.symm
theorem Ne.symm : ∀ {α : Sort u} {a b : α}, a ≠ b → b ≠ a
This theorem states that for all types `α` and for any two elements `a` and `b` of that type, if `a` is not equal to `b`, then `b` is not equal to `a`. In other words, inequality is symmetric in Lean, just as it is in Mathematics. If `a` and `b` are different, it doesn't matter in which order we consider them: the inequality holds either way.
More concisely: For all types `α` and for all `a` and `b` in `α`, if `a ≠ b` then `b ≠ a`.
|
le_of_le_of_eq
theorem le_of_le_of_eq : ∀ {α : Type u} {a b c : α} [inst : LE α], a ≤ b → b = c → a ≤ c
This theorem, named "le_of_le_of_eq", states that for any type `α` which has a less-than-or-equal-to (`≤`) relation, given three elements `a`, `b`, and `c` of this type, if `a` is less than or equal to `b` and `b` is equal to `c`, then `a` is less than or equal to `c`. This theorem is applying the transitivity of the less-than-or-equal-to relation in combination with the substitution property of equality.
More concisely: If `a ≤ b` and `b = c`, then `a ≤ c`.
|
eqRec_heq
theorem eqRec_heq : ∀ {α : Sort u} {φ : α → Sort v} {a a' : α} (h : a = a') (p : φ a), HEq (Eq.recOn h p) p
This theorem, `eqRec_heq`, states that for any type `α`, any type-dependent function `φ` from `α` to some other type, and any two elements `a` and `a'` of `α` with a proof `h` that `a` equals `a'`, and any element `p` of type `φ a`, the `HEq` relationship (heterogeneous equality, or equality between elements of possibly different types) holds between the element obtained by applying the `Eq.recOn` function with the equality `h` and the element `p`, and the original element `p` itself. In other words, we can "reconstruct" the original element `p` using the `Eq.recOn` function and the proof of equality `h`, and the result is heterogeneously equal to `p`.
More concisely: For any type `α`, type-dependent function `φ : α → *`, elements `a` and `a'` of `α` with proof `h : a = a'`, and element `p : φ a`, `Eq.recOn h p = p` holds up to heterogeneous equality.
|
Sum.inr.injEq
theorem Sum.inr.injEq : ∀ {α : Type u} {β : Type v} (val val_1 : β), (Sum.inr val = Sum.inr val_1) = (val = val_1) := by
sorry
This theorem, `Sum.inr.injEq`, states that for any two values (`val` and `val_1`) of type `β`, the assertion that `Sum.inr val` is equal to `Sum.inr val_1` is equivalent to the assertion that `val` is equal to `val_1`. The `Sum.inr` function wraps a value into the right side of a sum type, and this theorem assures that the equality of two such wrapped values depends solely on the equality of the values themselves, not on the wrapping function.
More concisely: For any type `β`, the equality of `Sum.inr (val : β)` and `Sum.inr (val_1 : β)` holds if and only if `val` is equal to `val_1`.
|
iff_false_left
theorem iff_false_left : ∀ {a b : Prop}, ¬a → ((a ↔ b) ↔ ¬b)
This theorem, `iff_false_left`, states that for any two propositions `a` and `b`, if `a` is not true (denoted as `¬a`), then the equivalence of `a` and `b` (denoted as `a ↔ b`) is equivalent to `b` not being true (denoted as `¬b`). In other words, if `a` is false, then `a` is equivalent to `b` if and only if `b` is also false.
More concisely: For all propositions `a` and `b`, `¬a ↔ (a ↔ b) ↔ ¬b`.
|
mt
theorem mt : ∀ {a b : Prop}, (a → b) → ¬b → ¬a
This theorem, which we will refer to as 'mt', states that for all propositions 'a' and 'b', if 'a' implies 'b' and 'b' is not true, then 'a' is also not true. In terms of logic, this is a basic statement of modus tollens: if we have a conditional statement ("if a then b") and the consequent ('b') is known to be false, then the antecedent ('a') must also be false.
More concisely: If `a` implies `b` and not `b`, then not `a`.
|
heq_of_eq
theorem heq_of_eq : ∀ {α : Sort u} {a a' : α}, a = a' → HEq a a'
This theorem, `heq_of_eq`, states that for any given type `α` and any two elements `a` and `a'` of that type, if `a` is equal to `a'` (denoted as `a = a'`), then `a` and `a'` are heterogeneously equal (denoted as `HEq a a'`). Here, "heterogeneously equal" means that the elements are equal, even if they may have different types, which in this specific theorem, they do not since they are both of the same type `α`. This theorem therefore establishes a direct connection between the normal equality and heterogeneous equality in Lean.
More concisely: For all types `α` and elements `a` and `a'` of type `α`, if `a` equals `a'` (`a = a'`), then `a` is heterogeneously equal to `a'` (`HEq a a'`).
|
Quotient.exists_rep
theorem Quotient.exists_rep : ∀ {α : Sort u} {s : Setoid α} (q : Quotient s), ∃ a, ⟦a⟧ = q
This theorem, `Quotient.exists_rep`, states that for any Sort `α` and any Setoid `s` on `α`, and for any Quotient `q` of `s`, there exists some element `a` from `α` such that the equivalence class of `a` under the Setoid `s` is equal to `q`. In other words, every quotient has a representative from the original set `α`.
More concisely: For any Setoid `s` on Sort `α` and its Quotient `q`, there exists an element `a` in `α` such that `q = [a]_s` (the equivalence class of `a` under `s`).
|
Thunk.sizeOf_eq
theorem Thunk.sizeOf_eq : ∀ {α : Type u_1} [inst : SizeOf α] (a : Thunk α), sizeOf a = 1 + sizeOf a.get
This theorem, `Thunk.sizeOf_eq`, states that for any type `α` equipped with a `SizeOf` instance and for any thunk `a` of type `Thunk α`, the size of `a` is equal to one plus the size of the value obtained by applying `Thunk.get` to `a`. In other words, the total size of a thunk includes 1 for the thunk itself, and the size of the actual value it computes.
More concisely: For any type `α` with `SizeOf` instance and `Thunk α` value `a`, `SizeOf.eq (Thunk.sizeOf a) (1 + SizeOf.of (Thunk.get a))`.
|
ne_comm
theorem ne_comm : ∀ {α : Sort u_1} {a b : α}, a ≠ b ↔ b ≠ a
This theorem, `ne_comm`, states that for any type or sort `α`, and any two elements `a` and `b` of type `α`, the proposition `a ≠ b` is equivalent to `b ≠ a`. In other words, if `a` is not equal to `b`, then `b` is not equal to `a`, and vice versa. This theorem applies to any type, not just numbers.
More concisely: For any type or sort `α` and elements `a`, `b` of type `α`, the proposition `a ≠ b` is equivalent to `b ≠ a`.
|
Quot.inductionOn
theorem Quot.inductionOn :
∀ {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (q : Quot r),
(∀ (a : α), motive (Quot.mk r a)) → motive q
This theorem is called 'Quotient Induction On', and it states that for any type `α`, a relation `r` on `α`, and a property `motive` defined on the quotient of `α` by `r`, if we know that this property holds for every element `a` of type `α` under the quotient mapping `Quot.mk r a`, then the property also holds for any element `q` in the quotient type `Quot r`. Essentially, it allows reasoning on the quotient type by considering representatives of each equivalence class under the relation `r`.
More concisely: If a property `motive` holds for all representatives `Quot.mk r a` of every equivalence class under relation `r` on type `α`, then the property holds for all elements `q` in the quotient type `Quot r`.
|
Nat.succ.injEq
theorem Nat.succ.injEq : ∀ (u v : ℕ), (u.succ = v.succ) = (u = v)
This theorem, `Nat.succ.injEq`, states that for any two natural numbers `n` and `n_1`, the equality of their successors (i.e., `Nat.succ n = Nat.succ n_1`) is equivalent to the equality of the numbers themselves (i.e., `n = n_1`). In other words, if the successors of two numbers are equal, then the numbers themselves are equal. This is a reflection of the injective (or one-to-one) property of the successor function on natural numbers.
More concisely: The successor function is injective on natural numbers, that is, for all natural numbers `n` and `n_1`, `Nat.succ n = Nat.succ n_1` implies `n = n_1`.
|
not_not_intro
theorem not_not_intro : ∀ {p : Prop}, p → ¬¬p
This theorem, `not_not_intro`, states that for any given proposition `p`, if `p` is true, then it is not the case that `p` is not true. In other words, it asserts the principle of double negation: if you have a proposition `p`, and `p` is true, then you cannot assert that it is not untrue. This is a fundamental concept in logic and proof theory.
More concisely: For all propositions p, p && ∼∼p. (In Lean syntax: `not_not p`)
|
Sum.inl.inj
theorem Sum.inl.inj : ∀ {α : Type u} {β : Type v} {val val_1 : α}, Sum.inl val = Sum.inl val_1 → val = val_1
This theorem, `Sum.inl.inj`, asserts that for any types `α` and `β`, and any values `val` and `val_1` of type `α`, if `Sum.inl val` is equal to `Sum.inl val_1`, then `val` must be equal to `val_1`. In simpler terms, it states that the left injection function (`Sum.inl`) of a sum type is injective, meaning that it faithfully represents different values: two different values cannot be mapped to the same result by this function.
More concisely: For all types `α` and values `val`, `val_1` of type `α`, if `Sum.inl val = Sum.inl val_1` in the type `Sum α`, then `val = val_1`.
|
Setoid.iseqv
theorem Setoid.iseqv : ∀ {α : Sort u} [self : Setoid α], Equivalence Setoid.r
This theorem states that, for any type `α` equipped with a `Setoid` structure (which is a type of structure in Lean 4 that specifies an equivalence relation), the relation `x ≈ y` (denoted as `Setoid.r` in Lean 4) is an equivalence relation. An equivalence relation in mathematics is a binary relation that is reflexive (every element is related to itself), symmetric (if `x` is related to `y`, then `y` is related to `x`), and transitive (if `x` is related to `y` and `y` is related to `z`, then `x` is related to `z`).
More concisely: Given a type `α` with a Setoid structure, the relation `x ≈ y` is an equivalence relation.
|
Iff.mpr
theorem Iff.mpr : ∀ {a b : Prop}, (a ↔ b) → b → a
This theorem states the reversed version of Modus Ponens for 'if and only if'. Given two propositions `a` and `b`, if we know that `a` is equivalent to `b` (denoted `a ↔ b`), and we also know that `b` is true, then we can conclude that `a` is also true. This theorem is a fundamental rule of inference in propositional logic.
More concisely: If `a ↔ b` and `b` are true, then `a` is true. (The reversed version of if and only if Modus Ponens in propositional logic.)
|
Equivalence.symm
theorem Equivalence.symm : ∀ {α : Sort u} {r : α → α → Prop}, Equivalence r → ∀ {x y : α}, r x y → r y x
This theorem states that an equivalence relation is symmetric. In other words, for any type `α` and any relation `r` on `α`, if `r` is an equivalence relation, then for any `x` and `y` of type `α`, if `x` is related to `y` by `r` (denoted as `r x y`), then `y` is also related to `x` (denoted as `r y x`). This is a fundamental property of equivalence relations in mathematics.
More concisely: If `r` is an equivalence relation on type `α`, then for all `x` and `y` of type `α`, `r x y` implies `r y x`.
|
IsLawfulSingleton.insert_emptyc_eq
theorem IsLawfulSingleton.insert_emptyc_eq :
∀ {α : Type u} {β : Type v} [inst : EmptyCollection β] [inst_1 : Insert α β] [inst_2 : Singleton α β]
[self : IsLawfulSingleton α β] (x : α), insert x ∅ = {x}
This theorem states that for any types `α` and `β`, given that `β` can be an empty collection, `α` can be inserted into `β`, `β` can be a singleton of `α`, and these operations obey certain laws (i.e., they are lawful), then inserting an element `x` of type `α` into an empty collection produces a singleton collection containing only `x`. In mathematical terms, it asserts that inserting `x` into the empty set results in a set that only contains `x`, i.e., `{x}`.
More concisely: Given any types `α` and `β` where `α` can be inserted into `β` and the related operations are lawful, inserting an element `x` of type `α` into an empty collection `β` yields a singleton collection `{x}`.
|
Subsingleton.elim
theorem Subsingleton.elim : ∀ {α : Sort u} [h : Subsingleton α] (a b : α), a = b
This theorem, `Subsingleton.elim`, states that for any sort `α` that is a subsingleton (that is, a type with at most one element), any two elements `a` and `b` of that type are equal. In other words, if a type is a subsingleton, it doesn't have distinct elements.
More concisely: If `α` is a subsingleton type, then for all `a` and `b` in `α`, `a = b`.
|
Decidable.of_not_not
theorem Decidable.of_not_not : ∀ {p : Prop} [inst : Decidable p], ¬¬p → p
This theorem is stating that for any proposition `p`, if `p` is decidable (meaning it is either true or false), then if it's not the case that `p` is not true (expressed as ¬¬p), it follows that `p` is true. In other words, if we can't deny that `p` is false, then `p` is true. This is a formulation of the law of double negation in classical logic.
More concisely: In classical logic, if a proposition `p` is decidable, then `p` and ¬¬`p` are logically equivalent.
|
Iff.of_eq
theorem Iff.of_eq : ∀ {a b : Prop}, a = b → (a ↔ b)
This theorem states that for any two propositions `a` and `b`, if `a` is equal to `b`, then `a` is logically equivalent to `b` (denoted as `a ↔ b`). This logical equivalence means that `a` implies `b` and `b` implies `a`. In other words, `a` and `b` both hold true or false under the same conditions.
More concisely: For all propositions `a` and `b`, `a = b` implies `a ↔ b`.
|
Quotient.sound
theorem Quotient.sound : ∀ {α : Sort u} {s : Setoid α} {a b : α}, a ≈ b → ⟦a⟧ = ⟦b⟧
This theorem, `Quotient.sound`, establishes that if two elements `a` and `b` from an arbitrary type `α` are related by an equivalence relation defined by `Setoid α`, then their equivalence classes (denoted by ⟦a⟧ and ⟦b⟧) are the same. In other words, if two items `a` and `b` are equivalent under a given equivalence relation, then they belong to the same equivalence class.
More concisely: If `a` and `b` are related by an equivalence relation `R` on type `α`, then `a R b` implies `⟦a⟧ = ⟦b⟧`.
|
Equivalence.trans
theorem Equivalence.trans : ∀ {α : Sort u} {r : α → α → Prop}, Equivalence r → ∀ {x y z : α}, r x y → r y z → r x z
This theorem states that an equivalence relation is transitive. In other words, for any type `α` and any relation `r` on `α` that satisfies the properties of an equivalence relation, if `x`, `y`, and `z` are elements of `α` and `x` is related to `y` (`x ~ y`) and `y` is related to `z` (`y ~ z`), then `x` is related to `z` (`x ~ z`). This is a property of equivalence relations that is fundamental to their definition.
More concisely: If `α` is a type and `r` is an equivalence relation on `α`, then for all `x`, `y`, and `z` in `α`, if `x ~ y` and `y ~ z`, then `x ~ z`.
|
PUnit.subsingleton
theorem PUnit.subsingleton : ∀ (a b : PUnit.{u_1}), a = b
This theorem states that for any two elements `a` and `b` of the type `PUnit`, `a` is always equal to `b`. In other words, `PUnit` is a subsingleton type, meaning it has at most one distinct element, so any two instances of `PUnit` must necessarily be equal.
More concisely: The type `PUnit` has at most one element, hence any two elements `a` and `b` of `PUnit` are equal: `a = b`.
|
Setoid.symm
theorem Setoid.symm : ∀ {α : Sort u} [inst : Setoid α] {a b : α}, a ≈ b → b ≈ a
This theorem, `Setoid.symm`, states that for any sort `α` that has a `Setoid` instance, if `a` and `b` are elements in `α` and `a` is equivalent to `b`, then `b` is equivalent to `a`. In other words, the equivalence relation (`≈`) in a Setoid is symmetric.
More concisely: For any Setoid `α`, if `a ≈ b` then `b ≈ a`.
|
Iff.symm
theorem Iff.symm : ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
This theorem, `Iff.symm`, states that for all propositions `a` and `b`, if `a` is logically equivalent to `b` (denoted as `a ↔ b`), then `b` is also logically equivalent to `a`. This is the principle of symmetry in logical equivalence, reflecting that if both `a` and `b` have the same truth values in all cases, their order doesn't matter. This is akin to saying if `a` is true whenever `b` is true and vice versa, then the reverse statement that `b` is true whenever `a` is true and vice versa also holds.
More concisely: If `a` is logically equivalent to `b`, then `b` is logically equivalent to `a`. (The principle of symmetric logical equivalence.)
|
Function.comp_apply
theorem Function.comp_apply :
∀ {β : Sort u_1} {δ : Sort u_2} {α : Sort u_3} {f : β → δ} {g : α → β} {x : α}, (f ∘ g) x = f (g x)
This theorem, named "Function.comp_apply", states that for every three types `β`, `δ`, and `α` and given any two functions `f : β → δ` and `g : α → β`, as well as any element `x` of type `α`, the composition of `f` and `g` applied to `x` (`(f ∘ g) x`) is equal to `f` applied to the result of `g` applied to `x` (`f (g x)`). This is essentially the definition of function composition in mathematics, often written as $(f \circ g)(x) = f(g(x))$.
More concisely: The theorem asserts that for functions `f : β → δ` and `g : α → β`, `(f ∘ g) x = f (g x)` for all `x : α`.
|
and_comm
theorem and_comm : ∀ {a b : Prop}, a ∧ b ↔ b ∧ a
This theorem, `and_comm`, states that for all propositions `a` and `b`, the logical conjunction of `a` and `b` is equivalent to the logical conjunction of `b` and `a`. In other words, the order does not matter in the 'and' operation; `a` and `b` is the same as `b` and `a`. This property is known as commutativity, hence the name `and_comm`.
More concisely: For all propositions `a` and `b`, `(a ∧ b)` is equivalent to `(b ∧ a)`.
|
true_ne_false
theorem true_ne_false : ¬True = False
This theorem states that `True` is not equal to `False`. In the context of propositional logic, `True` and `False` represent distinct truth values. Hence, they can't be equal, and this theorem formalizes that fact in Lean 4.
More concisely: The theorem asserts that `True` and `False` are distinct propositions in Lean 4.
|
iff_false_intro
theorem iff_false_intro : ∀ {a : Prop}, ¬a → (a ↔ False)
This theorem, `iff_false_intro`, states that for any proposition `a`, if `a` is not true (i.e., `¬a`), then `a` is equivalent to `False`. In other words, if we can prove that a given proposition is not true, we can conclude that this proposition is logically equivalent to `False`. This theorem is a fundamental concept in propositional logic.
More concisely: The theorem `iff_false_intro` asserts that for any proposition `a`, the negation of `a` is logically equivalent to `False`.
|
Bool.of_not_eq_true
theorem Bool.of_not_eq_true : ∀ {b : Bool}, ¬b = true → b = false
This theorem states that for any boolean value `b`, if `b` is not equal to `true`, then `b` must be equal to `false`. Remember that in the context of boolean logic, a variable can only have two possible values: `true` or `false`. Hence, if it's not `true`, it has to be `false`.
More concisely: If a boolean value is not true, then it is false.
|
beq_iff_eq
theorem beq_iff_eq : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (a b : α), (a == b) = true ↔ a = b := by
sorry
The theorem `beq_iff_eq` states that for any type `α` that has a `BEq` instance and respects the laws of `BEq`, the boolean equality of two elements `a` and `b` of type `α` (`a == b`) being true is equivalent to `a` and `b` being actually equal (`a = b`). This means that the boolean equality test `==` is accurate if it returns `true`, and `a` and `b` can be deemed equal in the mathematical sense.
More concisely: For any type `α` with a `BEq` instance satisfying the laws of `BEq`, `a == b` if and only if `a = b`.
|
if_pos
theorem if_pos : ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort u} {t e : α}, (if c then t else e) = t
This theorem, `if_pos`, states that for any proposition `c` and any decidable instance `h` of `c`, if `c` is true, then for any type `α` and any two instances `t` and `e` of this type, the expression `if c then t else e` will always evaluate to `t`. In other words, if the condition of an `if` statement is true, then the value of the whole `if` statement is the value of the `then` clause.
More concisely: Given a decidable proposition `c` and instances `t` and `e` of any type `α`, if `c` holds then `if c then t else e` evaluates to `t`.
|
Iff.mp
theorem Iff.mp : ∀ {a b : Prop}, (a ↔ b) → a → b
This theorem, Modus Ponens for if and only if, declares that if we have a bi-conditional proposition `a ↔ b` (i.e. `a` if and only if `b`), and we know `a` is true, then we can deduce that `b` is true. In other words, if `a` and `b` are logically equivalent and `a` is true, then `b` must also be true.
More concisely: If `a` is logically equivalent to `b` and `a` is true, then `b` is true.
|
gt_iff_lt
theorem gt_iff_lt : ∀ {α : Type u} [inst : LT α] {x y : α}, x > y ↔ y < x
This theorem, named `gt_iff_lt`, states that for any type `α` that has a less than (`<`) operation, and for any two elements `x` and `y` of this type, `x` is greater than `y` if and only if `y` is less than `x`. Basically, it formalizes the intuitive notion of the relationship between 'greater than' and 'less than' in any ordered type.
More concisely: For all types `α` with a `<` operation and all `x, y` in `α`, `x` is greater than `y` if and only if `y` is less than `x`.
|
cast_heq
theorem cast_heq : ∀ {α β : Sort u} (h : α = β) (a : α), HEq (cast h a) a
This theorem, `cast_heq`, asserts that for any two sorts `α` and `β` in Lean 4 (which can be thought of as types), if `α` is equal to `β` and `a` is an instance of `α`, then `a` cast to `β` (using the equality `h` as justification for the cast) is heterogeneously equal to `a`. In other words, not only is `a` equal to itself after the cast, but the cast version of `a` and the original `a` are considered to be the same kind of object. Here, "HEq" stands for heterogeneous equality, a notion of equality that allows for comparison of values of different types.
More concisely: For any types `α` and `β` in Lean 4, and for any `a` of type `α`, if `α` is equal to `β` and `a` has an instance of type `α`, then `a` and its cast to type `β` are heterogeneously equal.
|
LawfulBEq.rfl
theorem LawfulBEq.rfl : ∀ {α : Type u} [inst : BEq α] [self : LawfulBEq α] {a : α}, (a == a) = true
This theorem states that the equality comparison operator (`==`) is reflexive for any type `α` that supports binary equality (`BEq`). This means that for any element `a` of type `α`, when we compare `a` with itself using the `==` operator, the result is always `true`. This is a fundamental property of equality in mathematics and logic.
More concisely: For any type `α` with binary equality `BEq`, the reflexivity property holds: `a == a` for all `a : α`.
|
not_congr
theorem not_congr : ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
This theorem, `not_congr`, states that for any two propositions `a` and `b`, if `a` is logically equivalent to `b` (denoted as `a ↔ b`), then the negation of `a` (denoted as `¬a`) is also logically equivalent to the negation of `b` (denoted as `¬b`). In other words, if two statements are equivalent, their negations are also equivalent.
More concisely: If `a` is logically equivalent to `b`, then the negations `¬a` and `¬b` are logically equivalent.
|
Or.symm
theorem Or.symm : ∀ {a b : Prop}, a ∨ b → b ∨ a
This theorem, `Or.symm`, states that for all propositions `a` and `b`, if `a` or `b` is true then `b` or `a` is also true. In other words, the disjunction (logical "or") operation is symmetric, meaning that the order of the propositions doesn't affect the truth value of the disjunction.
More concisely: For all propositions `a` and `b`, `a ∨ b` is equivalent to `b ∨ a`.
|
Eq.substr
theorem Eq.substr : ∀ {α : Sort u} {p : α → Prop} {a b : α}, b = a → p a → p b
This is a theorem in the Lean 4 theorem prover about substituting equals with equals in logical expressions. In more detail, given a type α, a predicate p over α, and two elements a and b of type α, if b equals a, and if p holds for a, then p also holds for b. This theorem follows from the principle of substitutability, which states that if two values are equal, one can be substituted for the other in any formula without changing the truth of the formula.
More concisely: If a = b and p(a) is a proposition, then p(b) is propositionally equal to p(a).
|
imp_iff_right
theorem imp_iff_right : ∀ {b a : Prop}, a → (a → b ↔ b)
This theorem, `imp_iff_right`, states that for all propositions `a` and `b`, if `a` is true, then `a` implies `b` is equivalent to `b`. In other words, given that `a` is true, if `b` is true whenever `a` is true (i.e., `a` implies `b`), then `b` must be true; conversely, if `b` is true, then `a` implies `b` must also be true.
More concisely: For all propositions `a` and `b`, `a` implies `b` is logically equivalent to `(a → b) ≡ b`.
|
iff_true_intro
theorem iff_true_intro : ∀ {a : Prop}, a → (a ↔ True)
This theorem, "iff_true_intro", states that for any proposition 'a', if 'a' is true, then 'a' is logically equivalent to 'True'. In other words, if we have a proof of 'a', we can conclude that 'a' is both true and that 'True' implies 'a'. This theorem is a fundamental concept in propositional logic and a basic tool in the Lean 4 theorem prover.
More concisely: If a proposition 'a' is true, then 'a' is logically equivalent to 'True'.
|
LawfulBEq.eq_of_beq
theorem LawfulBEq.eq_of_beq : ∀ {α : Type u} [inst : BEq α] [self : LawfulBEq α] {a b : α}, (a == b) = true → a = b
This theorem, known as `LawfulBEq.eq_of_beq`, states that given any type `α` that has a binary equivalence relation (`BEq α`) and follows the lawful binary equivalence laws (`LawfulBEq α`), if the binary equivalence of two instances `a` and `b` of type `α` is `true`, then `a` and `b` are logically equal (i.e., `a = b`). In other words, it provides a way to translate from the binary equivalence relation (`a == b`) to logical equality (`a = b`) when the latter is `true`.
More concisely: Given a type `α` with a lawful binary equivalence relation `BEq α`, `a BEq b` implies `a = b`.
|
cast_eq
theorem cast_eq : ∀ {α : Sort u} (h : α = α) (a : α), cast h a = a
This theorem, named `cast_eq`, states that for any type `α` and any element `a` of that type, casting `a` to the same type `α` (using an equality proof `h` that `α` equals `α`) results in the same element `a`. In other words, casting an element to its original type doesn't change the element.
More concisely: For any type `α` and element `a` of type `α`, the conversion `a : α` is equal to `a`.
|
Subtype.eta
theorem Subtype.eta : ∀ {α : Type u} {p : α → Prop} (a : { x // p x }) (h : p ↑a), ⟨↑a, h⟩ = a
This theorem, `Subtype.eta`, states that for any type `α`, and any predicate `p` on `α`, given an element `a` of the subtype of `α` satisfying `p`, and a proof `h` that `a` satisfies `p`, constructing a new subtype element with value `a` and proof `h` yields the same element `a`. Essentially, it asserts that elements of a subtype are unambiguously characterized by their underlying element of the original type, with no duplication for different proofs of the same property.
More concisely: For any type `α` and predicate `p` on `α`, if `a : α` satisfies `p` and `h : p a`, then the elements `(a, h) : p.{max 1} α` and `a` are equal.
|
iff_iff_eq
theorem iff_iff_eq : ∀ {a b : Prop}, (a ↔ b) ↔ a = b
This theorem states that for any two propositions 'a' and 'b', the proposition that 'a' is logically equivalent to 'b' is itself logically equivalent to the proposition that 'a' equals 'b'. In other words, stating that two propositions are logically equivalent is the same as saying that they are equal.
More concisely: The proposition "a is logically equivalent to b" is equivalent to the proposition "a = b" for any propositions a and b.
|
Init.Core._auxLemma.1
theorem Init.Core._auxLemma.1 :
∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (a b : α), ((a == b) = true) = (a = b)
This theorem, named `Init.Core._auxLemma.1`, states that for any type `α` that has an instance of binary equality (`BEq α`) and is lawfully binary equal (`LawfulBEq α`), the binary equality comparison of any two elements `a` and `b` of this type, expressed as `(a == b) = true`, is equivalent to stating that `a` and `b` are equal in the standard sense `(a = b)`. This means that the binary equality operation correctly reflects the true equality of elements in the type `α`.
More concisely: For types endowed with lawful binary equality and instance of binary equality, binary equality implies standard equality.
|
Ne.irrefl
theorem Ne.irrefl : ∀ {α : Sort u} {a : α}, a ≠ a → False
This theorem, `Ne.irrefl`, states that for all types `α` and for all elements `a` of type `α`, it is not possible for `a` to not be equal to itself. In other words, it asserts the principle of self-identity, that everything is equal to itself, across all types. This is a formalization of the classical logic principle of contradiction, where a proposition cannot be both true and not true. In mathematical notation, this could be written as "for all α and for all a in α, ¬(a ≠ a)".
More concisely: For all types `α` and elements `a` of type `α`, `a` is equal to `a`.
|
dif_neg
theorem dif_neg : ∀ {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬c → α}, dite c t e = e hnc
The theorem `dif_neg` states that for any proposition `c`, given a proof `hnc` that `c` is not true (`¬c`), and two dependent functions `t` and `e` from `c` and `¬c` to any type `α` respectively, the `if-then-else` construct `dite` (which stands for "dependent if then else") will evaluate to `e hnc`. In other words, if `c` is false, `dite` ignores the function `t` and applies `e` to the proof of `¬c`.
More concisely: If `c` is false and we have a proof `hnc` of it, then the evaluation of `dite` with arguments `c`, `t`, and `e` is equal to the application of `e` to `hnc`.
|
imp_not_comm
theorem imp_not_comm : ∀ {a b : Prop}, a → ¬b ↔ b → ¬a
This theorem states that for any two propositions `a` and `b`, the implication of `a` leading to the negation of `b` is logically equivalent to `b` leading to the negation of `a`. In other words, if assuming `a` to be true implies that `b` must be false, then it is also true that if `b` is assumed true, `a` must be false, and vice versa. This captures a fundamental symmetry in logical reasoning.
More concisely: The logical implication `a → ⊥ → b` is equivalent to `b → ⊥ → a`, where `⊥` represents the logical false.
|
Iff.trans
theorem Iff.trans : ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
This theorem, `Iff.trans`, states that for any three propositions `a`, `b`, and `c`, if `a` is logically equivalent to `b`, and `b` is logically equivalent to `c`, then `a` is logically equivalent to `c`. This is a transitive property for logical equivalence in propositional logic. In mathematical terms, if we have $(a \iff b)$ and $(b \iff c)$, it follows that we have $(a \iff c)$.
More concisely: If `a` is logically equivalent to `b`, and `b` is logically equivalent to `c`, then `a` is logically equivalent to `c` (`(a ��CREF b) ∧ (b ��CREF c) ⊢ a ��CREF c` in Lean 4 syntax).
|
Quotient.ind₂
theorem Quotient.ind₂ :
∀ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Prop},
(∀ (a : α) (b : β), motive ⟦a⟧ ⟦b⟧) → ∀ (q₁ : Quotient s₁) (q₂ : Quotient s₂), motive q₁ q₂
The theorem `Quotient.ind₂` states that for any sorts `α` and `β` with setoids `s₁` and `s₂` respectively, and any property `motive` that relates two quotients, if this property holds for the equivalence classes of every pair of elements `(a, b)` from `α` and `β` respectively, then this property holds for every pair of quotients `(q₁, q₂)` from the respective quotient sets. Essentially, it allows you to prove a property about all pairs of elements in quotient sets by proving it for representatives of each equivalence class.
More concisely: If `motive` holds for the equivalence classes of every pair of elements in the sets `α / s₁` and `β / s₂`, then `motive` holds for the quotients `q₁` and `q₂` in the respective quotient sets.
|
Setoid.trans
theorem Setoid.trans : ∀ {α : Sort u} [inst : Setoid α] {a b c : α}, a ≈ b → b ≈ c → a ≈ c
This theorem states the transitivity property of a Setoid. In the context of any type `α` with a Setoid structure, for any three values `a`, `b`, and `c` of type `α`, if `a` is equivalent to `b` and `b` is equivalent to `c`, then `a` is equivalent to `c`. This is essentially a formalization of the transitivity of equivalence relations in the context of Setoids.
More concisely: If `α` is a type with a Setoid structure and `a`, `b`, and `c` are elements of `α`, then `a ≈ b` and `b ≈ c` imply `a ≈ c`.
|
Equivalence.refl
theorem Equivalence.refl : ∀ {α : Sort u} {r : α → α → Prop}, Equivalence r → ∀ (x : α), r x x
This theorem states that an equivalence relation is reflexive. In other words, for any type `α` and any relation `r` on `α` that is an equivalence relation, it holds that every element `x` of `α` is related to itself via `r`. In mathematical notation, this would be expressed as `∀x : α, r x x`.
More concisely: Every equivalence relation is reflexive, that is, for all `α` and `x ∈ α`, `x` is related to `x` via the relation `r`. In mathematical notation, `∀α : Type, ∀r : (α → α → Prop) (Equiv α), ∀x : α, r x x`.
|
iff_of_eq
theorem iff_of_eq : ∀ {a b : Prop}, a = b → (a ↔ b)
This theorem states that for any two propositions `a` and `b`, if `a` is equal to `b`, then `a` is logically equivalent to `b`. Here, logical equivalence is denoted by the double arrow (`↔`), and it means that `a` implies `b` and `b` implies `a`. In other words, `a` and `b` either both hold true or both hold false.
More concisely: For all propositions `a` and `b`, `a = b` if and only if `a ↔ b`.
|
iff_of_false
theorem iff_of_false : ∀ {a b : Prop}, ¬a → ¬b → (a ↔ b)
This theorem states that for any two propositions `a` and `b`, if `a` is not true and `b` is not true, then `a` is logically equivalent to `b`. In other words, if both `a` and `b` are false, then they are interchangeable in a logical sense.
More concisely: If `a` and `b` are propositions, then `a ⊬puisilon b ∧ b ⊬puisilon a` implies `a ↔ b`. (Here, `↔` denotes logical equivalence, and `⊬puisilon` denotes the negation of the implication.)
|
And.symm
theorem And.symm : ∀ {a b : Prop}, a ∧ b → b ∧ a
This theorem, `And.symm`, states that for all propositions `a` and `b`, if both `a` and `b` are true (denoted as `a ∧ b`), then it's also true that `b` and `a` are true (denoted as `b ∧ a`). In other words, the "and" operation (`∧`) is symmetric in the context of propositional logic.
More concisely: Given propositions `a` and `b`, if `a ∧ b` holds, then `b ∧ a` holds as well. (Or, equivalently, `a ∧ b` if and only if `b ∧ a`. )
|
not_false
theorem not_false : ¬False
This theorem, `not_false`, asserts that "not false" is true. In other words, it states that the negation of falsehood is a valid statement or true. This is a basic principle of logic, expressed here in the formal language of the Lean 4 theorem prover.
More concisely: The theorem `not_false` asserts that the negation of false is true. In mathematical terms, this is equivalent to saying that ⊥ (the logical false) and ⊥⊥ (the negation of logical false) are equivalent.
|
Option.some.inj
theorem Option.some.inj : ∀ {α : Type u} {val val_1 : α}, some val = some val_1 → val = val_1
This theorem, `Option.some.inj`, states that for all types `α` and for any two values `val` and `val_1` of that type, if `some val` equals `some val_1`, then `val` must equal `val_1`. Essentially, it ensures the injectivity of the `some` constructor of the `Option` type in Lean: distinct values get mapped to distinct `Option` values.
More concisely: If `Option.some val = Option.some val_1` for types `α` and values `val` and `val_1` of type `α`, then `val = val_1`.
|
Nat.add_zero
theorem Nat.add_zero : ∀ (n : ℕ), n + 0 = n
This theorem, `Nat.add_zero`, states that for any natural number `n`, the sum of `n` and zero is `n`. In other words, adding zero to any natural number doesn't change the value of the natural number. This is a fundamental property of addition, known as the identity property.
More concisely: For all natural numbers n, n + 0 = n.
|
lt_of_eq_of_lt
theorem lt_of_eq_of_lt : ∀ {α : Type u} {a b c : α} [inst : LT α], a = b → b < c → a < c
This theorem states that for any type `α` that has a less than operation, if you have three instances of this type `a`, `b`, and `c` such that `a` is equal to `b` and `b` is less than `c`, then `a` is less than `c`. This captures the intuitive idea that equality and the less than relation can be combined: if one thing equals another, and that other thing is less than a third thing, then the first thing is also less than the third thing.
More concisely: For any type `α` with a total order, if `a = b` and `b < c`, then `a < c`.
|
Quotient.inductionOn₃
theorem Quotient.inductionOn₃ :
∀ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid φ}
{motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂)
(q₃ : Quotient s₃), (∀ (a : α) (b : β) (c : φ), motive ⟦a⟧ ⟦b⟧ ⟦c⟧) → motive q₁ q₂ q₃
This theorem, `Quotient.inductionOn₃`, provides a principle of induction for three quotient types. Given any three sort types `α`, `β` and `φ` with setoid relations `s₁`, `s₂` and `s₃` respectively, it states that for any property `motive` that applies to the respective quotient types, if this property holds for representatives `a` from `α`, `b` from `β`, and `c` from `φ`, then it also holds for any elements `q₁`, `q₂` and `q₃` of the respective quotient types. Thus, it allows us to reason about all elements of these quotient types by only considering a representative element from each equivalence class.
More concisely: Given equivalence relations `s₁` on type `α`, `s₂` on type `β`, and `s₃` on type `φ`, if a property holds for representatives from each equivalence class, then it holds for all elements in the quotient types `α / s₁`, `β / s₂`, and `φ / s₃`.
|
Decidable.byContradiction
theorem Decidable.byContradiction : ∀ {p : Prop} [dec : Decidable p], (¬p → False) → p
This theorem, `Decidable.byContradiction`, states that for any proposition `p` which we can decide as either true or false (`Decidable p`), if we assume that the negation of `p` leads to a contradiction (expressed as `¬p → False`), then `p` must be true. In other words, it states the principle of proof by contradiction: if the assumption that `p` is not true leads to an impossibility, then `p` must be true. This is a fundamental principle in many areas of mathematics.
More concisely: If `p` is a decidable proposition and assuming `¬p` leads to a contradiction, then `p` is true.
|
beq_false_of_ne
theorem beq_false_of_ne : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a b : α}, a ≠ b → (a == b) = false
This theorem, `beq_false_of_ne`, states that for any type `α`, that has an instance of binary equality (`BEq`) and this binary equality is lawful (`LawfulBEq`), if two elements `a` and `b` of type `α` are not equal, then the result of the binary equality test (`a == b`) will be `false`. Essentially, it says that if two objects are not equal, their binary equality test result is `false`.
More concisely: For any type `α` with lawful equality `BEq α`, if `a ≠ b` then `a == b` holds false.
|
Quot.exists_rep
theorem Quot.exists_rep : ∀ {α : Sort u} {r : α → α → Prop} (q : Quot r), ∃ a, Quot.mk r a = q
This theorem, `Quot.exists_rep`, states that for any type `α` and any equivalence relation `r` on `α`, for every element `q` of the quotient type `Quot r` (the type of equivalence classes of `α` under `r`), there exists an element `a` of `α` such that `a` is a representative of the equivalence class `q`. In other words, each equivalence class in the quotient type `Quot r` has at least one representative element in the original type `α`.
More concisely: For every equivalence relation `r` on type `α` and every equivalence class `q` in the quotient `Quot r`, there exists a representative `a` in `α` such that `a` is related to every element in `q` under `r`.
|
Eq.propIntro
theorem Eq.propIntro : ∀ {a b : Prop}, (a → b) → (b → a) → a = b
This theorem, `Eq.propIntro`, states that for any two propositions `a` and `b`, if `a` implies `b` and `b` implies `a`, then `a` and `b` are equivalent, or in other words, `a = b`. This principle is commonly known as the equivalence of propositions. This is a fundamental concept in logic and is used throughout mathematics and computer science.
More concisely: If two propositions `a` and `b` imply each other, then `a` is equivalent to `b`, denoted as `a <-> b`.
|
Quotient.inductionOn
theorem Quotient.inductionOn :
∀ {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} (q : Quotient s), (∀ (a : α), motive ⟦a⟧) → motive q
The `Quotient.inductionOn` theorem states that for any type `α` and any equivalence relation `s` on `α`, for any property `motive` that we might want to prove about elements of the quotient type `Quotient s` and any element `q` of `Quotient s`, if we can prove the property for elements of the form `⟦a⟧` (where `a` is any element of `α`), then we can conclude that the property holds for `q`. In essence, this theorem provides an induction principle to reason about elements in the quotient type `Quotient s`, asserting that every element is in the equivalence class of some `a` from `α`.
More concisely: Given an equivalence relation `s` on type `α`, if a property `motive` holds for all `⟦a⟧` in `Quotient s` for some `a` in `α`, then the property holds for any `q` in `Quotient s`.
|
Iff.comm
theorem Iff.comm : ∀ {a b : Prop}, (a ↔ b) ↔ (b ↔ a)
This theorem, `Iff.comm`, states that for all propositions `a` and `b`, the biconditional statement "if and only if" ('↔') is commutative. In other words, the proposition "a if and only if b" is logically equivalent to the proposition "b if and only if a".
More concisely: The biconditional relation "a ↔ b" is an equivalence relation and is therefore commutative.
|
lt_of_lt_of_eq
theorem lt_of_lt_of_eq : ∀ {α : Type u} {a b c : α} [inst : LT α], a < b → b = c → a < c
This theorem, `lt_of_lt_of_eq`, states that for any type `α` that has a less than (`<`) operation, if an element `a` of that type is less than another element `b`, and `b` is equal to a third element `c`, then `a` is less than `c`. Essentially, it is a statement about transitivity of the less than operation in the presence of equality.
More concisely: If `a < b` and `b = c`, then `a < c`.
|
or_comm
theorem or_comm : ∀ {a b : Prop}, a ∨ b ↔ b ∨ a
This theorem, `or_comm`, states that for all propositions `a` and `b`, the logical disjunction `a ∨ b` (read as "a or b") is logically equivalent to `b ∨ a` (read as "b or a"). In other words, the order of the propositions in a disjunction operation does not affect the truth value of the disjunction, making the operation commutative.
More concisely: For all propositions `a` and `b`, the logical disjunction `a ∨ b` is equivalent to `b ∨ a`.
|
iff_def
theorem iff_def : ∀ {a b : Prop}, (a ↔ b) ↔ (a → b) ∧ (b → a)
This theorem states that for all propositions 'a' and 'b', the biconditional 'a if and only if b' is equivalent to the conjunction of 'if a then b' and 'if b then a'. Put simply, 'a' is equivalent to 'b' if 'a' implies 'b' and 'b' implies 'a'.
More concisely: The biconditional "a if and only if b" is logically equivalent to the conjunction of "if a then b" and "if b then a".
|
List.cons.injEq
theorem List.cons.injEq :
∀ {α : Type u} (head : α) (tail : List α) (head_1 : α) (tail_1 : List α),
(head :: tail = head_1 :: tail_1) = (head = head_1 ∧ tail = tail_1)
This theorem, `List.cons.injEq`, states that for any type `α`, given two heads `head` and `head_1` of this type, and two lists `tail` and `tail_1` of this type, the equality of the lists formed by prepending these heads to these tails (i.e., `head :: tail` and `head_1 :: tail_1`) is equivalent to the conjunction of the equality of the heads and the equality of the tails. In other words, two lists are equal if and only if their heads are equal and their tails are equal.
More concisely: For any type `α`, the list `cons x xs` equals the list `cons y ys` if and only if `x = y` and `xs = ys`.
|
if_neg
theorem if_neg : ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort u} {t e : α}, (if c then t else e) = e
This theorem states that for any proposition `c` and `Decidable c` instance `h`, if `c` is not true (i.e., `¬c`), then for any sort `α` and any two instances `t` and `e` of that sort, the expression `if c then t else e` will evaluate to `e`. In more layman's terms, it describes the logical behavior of an "if-then-else" statement: if the condition is not true, the "else" part is returned.
More concisely: If `c` is a propositional variable with decidable instance `h` and `c` is false, then `if c then t else e` evaluates to `e` for any values `t` and `e` of sort `α`.
|