right_comm
theorem right_comm : ∀ {α : Type u} (f : α → α → α), Commutative f → Associative f → RightCommutative f
The theorem `right_comm` states that for any type `α` and a binary operation `f` on `α`, if `f` is commutative, meaning it satisfies the property that for all `a` and `b` in `α`, `f(a, b) = f(b, a)`, and if `f` is associative, meaning it satisfies the property that for all `a`, `b`, and `c` in `α`, `f(f(a, b), c) = f(a, f(b, c))`, then `f` is right commutative. In the context of this theorem, right commutative means that for all `b`, `a₁`, and `a₂` in `α`, `f(f(b, a₁), a₂) = f(f(b, a₂), a₁)`.
More concisely: If a binary operation `f` on a type `α` is both commutative and associative, then it is right commutative.
|
false_or_iff
theorem false_or_iff : ∀ (p : Prop), False ∨ p ↔ p
This theorem states that for any proposition `p`, the logical disjunction of `False` and `p` is equivalent to `p`. In simpler terms, either something false or `p` is true if and only if `p` is true. This makes sense since a false statement cannot contribute to the truth of a disjunction.
More concisely: The theorem asserts that `False \|\ p` is equivalent to `p` for any proposition `p` in Lean.
|
not_of_not_not_not
theorem not_of_not_not_not : ∀ {a : Prop}, ¬¬¬a → ¬a
This theorem, `not_of_not_not_not`, states that for all propositions `a`, if it is not true that it is not true that `a` is not true (i.e., ¬¬¬a), then `a` is not true (i.e., ¬a). In other words, it is an alias of the forward direction of the `not_not_not` theorem, providing a direct way to infer the negation of a proposition from a triple negation of the same proposition.
More concisely: If not (not (not p)), then not p. (In other words, the triple negation of a proposition is equivalent to its negation.)
|
exists_unique_of_exists_of_unique
theorem exists_unique_of_exists_of_unique :
∀ {α : Sort u} {p : α → Prop}, (∃ x, p x) → (∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂) → ∃! x, p x
The theorem `exists_unique_of_exists_of_unique` states that for any sort `α` and any property `p` of `α`, if there exists an `α` that satisfies the property `p` (i.e., `(∃ x, p x)`) and for any two elements `y₁` and `y₂` which satisfy the property `p`, they are in fact the same (i.e., `(∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂)`), then there exists a unique `α` that satisfies the property `p`. Simply put, if there exists at least one element with a certain property, and no two different elements can both have this property, then there is exactly one element with this property.
More concisely: If there exists a unique element with a property in a sort, then there exists that element.
|
left_comm
theorem left_comm : ∀ {α : Type u} (f : α → α → α), Commutative f → Associative f → LeftCommutative f
The theorem `left_comm` states that for any type `α` and any binary function `f` on this type, if `f` is commutative and associative, then `f` is left commutative. In other words, for any two elements `a₁` and `a₂` of type `α` and any element `b` of some type `β`, the result of applying `f` to `a₁` and then applying `f` to the result and `a₂` is the same as applying `f` to `a₂` and then applying `f` to `a₁` and the result. This encapsulates the property that `f` can be rearranged or swapped in its arguments without changing the result when nested to the left.
More concisely: If a binary function `f` on type `α` is commutative and associative, then for all `a₁, a₂ : α` and `b : β`, `f a₁ (f a₂ b) = f a₂ (f a₁ b)`.
|
false_and_iff
theorem false_and_iff : ∀ (p : Prop), False ∧ p ↔ False
This theorem states that for any given proposition `p`, the conjunction of `False` and `p` is logically equivalent to `False`. In other words, if you have a statement that is `False` AND something else (regardless of whether that something else is true or false), the overall statement will always be false. This is a fundamental principle of logic known as "and-falsity".
More concisely: For all propositions p, False and p are logically equivalent. (Or equivalently, the conjunction of False and p is equal to False.)
|
ExistsUnique.intro
theorem ExistsUnique.intro : ∀ {α : Sort u_1} {p : α → Prop} (w : α), p w → (∀ (y : α), p y → y = w) → ∃! x, p x := by
sorry
This theorem, named `ExistsUnique.intro`, states that for any type `α` and any proposition `p` that depends on `α`, given an element `w` of type `α` for which the proposition `p` holds, and assuming that `w` is the unique element of type `α` for which proposition `p` holds, there exists a unique `x` such that the proposition `p` holds for `x`. This basically asserts the existence and uniqueness of an element satisfying a certain proposition.
More concisely: Given a type `α` and a proposition `p(α)` depending on `α`, if there exists a unique `w` of type `α` such that `p(w)` holds, then there exists a unique `x` of type `α` with `p(x)` holding.
|
Decidable.by_contradiction
theorem Decidable.by_contradiction : ∀ {p : Prop} [dec : Decidable p], (¬p → False) → p
This theorem, called `Decidable.by_contradiction`, is essentially an alias for `Decidable.byContradiction`. It states that for any proposition `p`, given that `p` is decidable (i.e., it is either true or false), if assuming `¬p` (the negation of `p`) leads to a contradiction (represented by `False`), then `p` must be true. This theorem represents the classic principle of proof by contradiction in logic.
More concisely: If `p` is a decidable proposition and assuming `¬p` leads to a contradiction, then `p` is true.
|
and_false_iff
theorem and_false_iff : ∀ (p : Prop), p ∧ False ↔ False
This theorem states that for any proposition `p`, the conjunction of `p` and `False` is logically equivalent to `False`. In other words, the statement "`p` and `False`" is always false, regardless of the truth value of `p`. This is a basic result in propositional logic, reflecting the fact that a conjunction is only true if both of its components are true.
More concisely: For all propositions p, p and False are logically equivalent to False.
|
ExistsUnique.unique
theorem ExistsUnique.unique : ∀ {α : Sort u} {p : α → Prop}, (∃! x, p x) → ∀ {y₁ y₂ : α}, p y₁ → p y₂ → y₁ = y₂ := by
sorry
The theorem `ExistsUnique.unique` states that for all types `α`, there is at most one element `x` of `α` that satisfies a certain property `p`. More specifically, if we know that there exists a unique `x` such that `p(x)` is true, then for any two elements `y₁` and `y₂` of `α`, if `p(y₁)` and `p(y₂)` are both true, then `y₁` and `y₂` must be equal. This theorem essentially formalizes the concept of uniqueness in Lean.
More concisely: If `α` has at most one element `x` satisfying `p(x)`, then for all `y₁, y₂ ∈ α`, if `p(y₁)` and `p(y₂)` hold, then `y₁ = y₂`.
|
true_and_iff
theorem true_and_iff : ∀ (p : Prop), True ∧ p ↔ p
The theorem `true_and_iff` states that for any proposition `p`, the logical AND of `True` and `p` is logically equivalent to `p` itself. In mathematical terms, we can express this as: for any proposition `p`, `True ∧ p` if and only if `p`. Basically, it means that combining any proposition with `True` using a logical AND does not change the truth value of the proposition.
More concisely: For any proposition `p`, `True ∧ p` is logically equivalent to `p`.
|
not_or_of_not
theorem not_or_of_not : ∀ {a b : Prop}, ¬a → ¬b → ¬(a ∨ b)
This theorem states that for any two propositions `a` and `b`, if `a` is not true (denoted `¬a`) and `b` is not true (denoted `¬b`), then the statement "either `a` or `b` is true" (denoted `a ∨ b`) is not true. In other words, the denial of each of two propositions implies the denial of their disjunction.
More concisely: ∀ (a b : Prop), ¬a ∧ ¬b → ¬(a ∨ b)
(This statement says that for all propositions a and b, if not-a and not-b hold then not (a or b) holds)
|
or_false_iff
theorem or_false_iff : ∀ (p : Prop), p ∨ False ↔ p
This theorem states that for any given proposition "p", the logical disjunction (or) of "p" and "false" is logically equivalent to "p". In other words, saying that either "p" is true or "false" is true, is the same as saying "p" is true, because "false" is always false and doesn't affect the outcome of the disjunction.
More concisely: For any proposition p, p ∨ false is logically equivalent to p.
|
Decidable.not_not_iff
theorem Decidable.not_not_iff : ∀ {p : Prop} [inst : Decidable p], ¬¬p ↔ p
This theorem, `Decidable.not_not_iff`, is an alias for `Decidable.not_not`. It states that for any proposition `p`, given that `p` is decidable, the double negation of `p` (i.e., `¬¬p`) is logically equivalent to `p` itself. In other words, if `p` is either true or false (decidable), then stating that it is not true that `p` is not true is the same as stating `p` is true. This theorem aligns with the principle of double negation in classic logic.
More concisely: For any decidable proposition `p`, `¬¬p` is logically equivalent to `p`.
|
and_true_iff
theorem and_true_iff : ∀ (p : Prop), p ∧ True ↔ p
The theorem `and_true_iff` states that for any proposition `p`, the conjunction of `p` and `True` is logically equivalent to `p` itself. This is based on the logical trait of True, which doesn't affect the truth value when conjoined with any other proposition. Essentially, it says that if you have a statement and true, it's just the same as the statement by itself.
More concisely: For all propositions p, p ∧ True is logically equivalent to p.
|
eq_rec_heq
theorem eq_rec_heq : ∀ {α : Sort u} {φ : α → Sort v} {a a' : α} (h : a = a') (p : φ a), HEq (Eq.recOn h p) p
The theorem `eq_rec_heq` states that for any type `α`, any function `φ` from `α` to some other type, and any two elements `a` and `a'` of `α` such that `a` equals `a'`, the heterogeneous equality (`HEq`) between an application of `Eq.recOn` with arguments `h` (the proof of `a = a'`) and `p` (an element of the type φ `a`), and `p` itself, holds. Essentially, the theorem is stating that `Eq.recOn` does not change the given element `p` when the equality proof `h` is used.
More concisely: For any type `α`, function `φ : α →Type _, elements `a` and `a'` of `α` with `a = a'`, and `p : φ a`, `Eq.recOn h p = p`, where `h : a = a'` is a proof of equality.
|
iff_true_iff
theorem iff_true_iff : ∀ {a : Prop}, (a ↔ True) ↔ a
This theorem states that for any proposition 'a', the biconditional (a ↔ True) is equivalent to the proposition 'a' itself. In plain words, it means that if 'a' is equivalent to 'True', then 'a' must be true, and vice versa. This theorem hence acts like a bridge between the logical equivalence to 'True' and the truth of a proposition.
More concisely: For any proposition 'a' in Lean, 'a' is logically equivalent to 'a' ↔ True.
|
iff_false_iff
theorem iff_false_iff : ∀ {a : Prop}, (a ↔ False) ↔ ¬a
This theorem states that for any proposition 'a', the biconditional of 'a' and 'False' is equivalent to the negation of 'a'. In other words, 'a' is equivalent to 'False' if and only if 'a' is not true.
More concisely: For all propositions 'a', 'a' is equivalent to False if and only if not 'a'.
|
if_congr
theorem if_congr :
∀ {α : Sort u} {b c : Prop} [inst : Decidable b] [inst_1 : Decidable c] {x y u v : α},
(b ↔ c) → x = u → y = v → (if b then x else y) = if c then u else v
This theorem, `if_congr`, states that for any sort `α`, propositions `b` and `c`, and elements `x`, `y`, `u`, and `v` of `α`, provided that `b` and `c` are decidable, if `b` is equivalent to `c` (`b` iff `c`), and `x` is equal to `u` and `y` is equal to `v`, then the conditional expression "if `b` then `x` else `y`" is equal to "if `c` then `u` else `v`". Essentially, this means that if the conditions and corresponding values of two conditional expressions are equivalent, the two expressions are also equivalent.
More concisely: If `b` is equivalent to `c`, and `x = u` and `y = v`, then the conditional expressions "if `b` then `x` else `y`" and "if `c` then `u` else `v`" are equal.
|
ExistsUnique.exists
theorem ExistsUnique.exists : ∀ {α : Sort u_1} {p : α → Prop}, (∃! x, p x) → ∃ x, p x
This theorem states that for any type `α` and any property `p` of `α`, if there exists a unique `x` of type `α` for which the property `p` is true (denoted as `∃! x, p x`), then there exists at least one `x` such that the property `p` is true (denoted as `∃ x, p x`). Essentially, it says that if something is uniquely true for a particular element, then it is at least true for one element.
More concisely: If there exists a unique element `x` of type `α` with property `p`, then there exists at least one element `x` of type `α` with property `p`.
|