not_or_intro
theorem not_or_intro : ∀ {a b : Prop}, ¬a → ¬b → ¬(a ∨ b)
This theorem, `not_or_intro`, states that for any two propositions `a` and `b`, if `a` is not true (denoted as `¬a`) and `b` is not true (denoted as `¬b`), then neither `a` nor `b` can be true (denoted as `¬(a ∨ b)`). In other words, it establishes that the negation of a disjunction (an 'or' statement) can be derived from the negations of its individual components.
More concisely: The negation of the disjunction of two propositions is logically equivalent to the conjunction of their negations.
|
not_and_of_not_left
theorem not_and_of_not_left : ∀ {a : Prop} (b : Prop), ¬a → ¬(a ∧ b)
This theorem states that for any two logical propositions `a` and `b`, if `a` is not true (denoted as `¬a`), then the combined statement "`a` and `b`" (denoted as `a ∧ b`) is also not true (denoted as `¬(a ∧ b)`). In other words, if we know that `a` is false, then any statement saying both `a` and `b` are true must also be false. This is a fundamental principle in classical logic.
More concisely: The negation of the conjunction of two propositions is logically equivalent to the negation of each proposition.
|
or_congr
theorem or_congr : ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∨ b ↔ c ∨ d)
This theorem, `or_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 logical disjunction `a OR b` is equivalent to the logical disjunction `c OR d`. In the language of propositional logic, if we know that two pairs of propositions are equivalent, then the "OR" of each pair is also equivalent.
More concisely: If `a` is logically equivalent to `c` and `b` is logically equivalent to `d`, then `aOrb` is logically equivalent to `cOrd` in propositional logic.
|
not_exists
theorem not_exists : ∀ {α : Sort u_1} {p : α → Prop}, (¬∃ x, p x) ↔ ∀ (x : α), ¬p x
This theorem, `not_exists`, states that for any type `α` and any proposition `p` that depends on `α`, the negation of the existence of an element of `α` that makes `p` true is equivalent to saying that for all elements of `α`, `p` is not true. In other words, there is no `x` in `α` for which `p` is true if and only if for every `x` in `α`, `p` is not true.
More concisely: For any type `α` and proposition `p` depending on `α`, `∀x ∈ α, ¬p x` is equivalent to `∃x ∈ α. ¬p x`.
|
ite_not
theorem ite_not :
∀ {α : Sort u_1} (p : Prop) [inst : Decidable p] (x y : α), (if ¬p then x else y) = if p then y else x
This theorem states that the negation of a condition `P` in an `if-then-else` (abbreviated as `ite`) expression is equivalent to swapping the branches of the `ite`. In more detail, for any type `α`, any proposition `P`, any decidable instance of `P`, and any two instances `x_1`, `y` of `α`, the value of the `ite` expression which checks if `P` is not true and returns `x_1` if so and `y` otherwise, is the same as the value of the `ite` expression which checks if `P` is true and returns `y` if so and `x_1` otherwise.
More concisely: For any type `α`, proposition `P`, decidable `P`, and instances `x_1`, `y` of `α`, `ite (not P) x_1 y` is equal to `ite P y x_1`.
|
Decidable.not_or_of_imp
theorem Decidable.not_or_of_imp : ∀ {a b : Prop} [inst : Decidable a], (a → b) → ¬a ∨ b
The theorem `Decidable.not_or_of_imp` states that for any two propositions `a` and `b`, given that `a` is decidable, if `a` implies `b` then either `not a` or `b` holds. This theorem connects logic implication with the logical disjunction, stating that if the truth of `b` follows from the truth of `a`, then either `a` is not true or `b` is true.
More concisely: If `a` is decidable and `a` implies `b`, then `not a` or `b` holds.
|
and_and_and_comm
theorem and_and_and_comm : ∀ {a b c d : Prop}, (a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d
This theorem states that for any four propositions `a`, `b`, `c`, and `d`, the logical conjunctions of these propositions are commutative under a specific pattern. That is, having `a` and `b` together, and `c` and `d` separately, is equivalent to having `a` and `c` together, and `b` and `d` separately. In other words, $(a \land b) \land c \land d$ is logically equivalent to $(a \land c) \land b \land d$.
More concisely: The theorem asserts the commutativity of logical conjunction for four propositions, that is, $(a \land b) \land c \land d \equiv (a \land c) \land b \land d$.
|
or_congr_left
theorem or_congr_left : ∀ {a b c : Prop}, (a ↔ b) → (a ∨ c ↔ b ∨ c)
This theorem, `or_congr_left`, states that for any three propositions `a`, `b`, and `c`, if `a` is equivalent to `b` (denoted as `a ↔ b`), then the disjunction of `a` and `c` is equivalent to the disjunction of `b` and `c` (denoted as `a ∨ c ↔ b ∨ c`). In other words, if two propositions are equivalent, we can replace one with the other in a disjunction without changing the truth value of the disjunction.
More concisely: If `a ↔ b`, then `a ∨ c ↔ b ∨ c`.
|
forall₃_congr
theorem forall₃_congr :
∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {p q : (a : α) → (b : β a) → γ a b → Prop},
(∀ (a : α) (b : β a) (c : γ a b), p a b c ↔ q a b c) →
((∀ (a : α) (b : β a) (c : γ a b), p a b c) ↔ ∀ (a : α) (b : β a) (c : γ a b), q a b c)
This theorem, named `forall₃_congr`, states that for any types `α`, `β` (which is dependent on `α`), and `γ` (which is dependent on both `α` and `β`), if you have two predicates `p` and `q` which take three arguments (an element of `α`, an element of `β`, and an element of `γ`), then the following is true: if for all such elements, `p` holds if and only if `q` holds, then the proposition stating that `p` holds for all such elements is equivalent to the proposition that `q` holds for all such elements. In other words, if `p` and `q` are equivalent for all elements, then the universality of `p` is equivalent to the universality of `q`.
More concisely: If for all `α`, `β`, and elements `x : α`, `y : β`, `p(x, y) ≡ q(x, y)` implies `∀ x, ∀ y, p(x, y) ↔ q(x, y)`.
|
Decidable.not_imp_not
theorem Decidable.not_imp_not : ∀ {a b : Prop} [inst : Decidable a], ¬a → ¬b ↔ b → a
This theorem states that for any two propositions `a` and `b`, given that `a` is decidable, the statement "not `a` implies not `b`" is logically equivalent to "if `b` then `a`". This theorem is essentially a formalization of the contrapositive law in propositional logic, which states that given two propositions `p` and `q`, the statement "if not `p` then not `q`" is equivalent to "if `q` then `p`". The condition that `a` is decidable is needed in the context of constructive logic, where not all propositions are assumed to be either true or false.
More concisely: In constructive logic, `not a` is logically equivalent to `∥a → b∥` given the decidability of `a`, where `→` denotes logical implication.
|
and_not_self_iff
theorem and_not_self_iff : ∀ (a : Prop), a ∧ ¬a ↔ False
This theorem states that for any proposition 'a', the conjunction of 'a' and the negation of 'a' is logically equivalent to 'False'. This is derived from the principle of contradiction in classical logic, which asserts that a proposition cannot be both true and not true at the same time.
More concisely: For all propositions 'a' in Lean 4, 'a' and the negation of 'a' are logically equivalent to False.
|
Decidable.not_iff_not
theorem Decidable.not_iff_not : ∀ {a b : Prop} [inst : Decidable a] [inst : Decidable b], (¬a ↔ ¬b) ↔ (a ↔ b) := by
sorry
The theorem `Decidable.not_iff_not` states that for any two propositions `a` and `b`, given that `a` and `b` are decidable (i.e., either `a` or `¬a` is true, and either `b` or `¬b` is true), the equivalence of the negations of `a` and `b` (i.e., `¬a` is equivalent to `¬b`) if and only if `a` is equivalent to `b`. In mathematical terms, for all propositions `a` and `b`, `(¬a ↔ ¬b) ↔ (a ↔ b)`.
More concisely: The negations of propositions `a` and `b` are equivalent if and only if `a` and `b` are equivalent, given that `a` and `b` are decidable.
|
and_congr_left'
theorem and_congr_left' : ∀ {a b c : Prop}, (a ↔ b) → (a ∧ c ↔ b ∧ c)
This theorem states that for any three propositions `a`, `b`, and `c`, if `a` is logically equivalent to `b` (denoted as `a ↔ b`), then the logical conjunction of `a` and `c` (denoted as `a ∧ c`) is logically equivalent to the logical conjunction of `b` and `c` (denoted as `b ∧ c`). In other words, if `a` and `b` can be substituted for each other in a logical context, then `a` and `b` can also be substituted for each other when both are conjoined with the same third proposition, `c`.
More concisely: If `a ↔ b`, then `a ∧ c ↔ b ∧ c`.
|
exists_and_left
theorem exists_and_left : ∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, (∃ x, b ∧ p x) ↔ b ∧ ∃ x, p x
This theorem, `exists_and_left`, states that for any type `α`, any predicate `p` applied to `α`, and any proposition `b`, the existence of an element of type `α` that satisfies both proposition `b` and predicate `p`, is logically equivalent to the situation where proposition `b` is true and there exists an element of type `α` that satisfies predicate `p`. In other words, the conjunction of a proposition and an existential quantification is commutative.
More concisely: For any type α, proposition b, and predicate p on α, the existence of an element x : α satisfying p(x) and b is logically equivalent to the existence of an element x : α satisfying p(x) and b is true.
|
exists_prop
theorem exists_prop : ∀ {b a : Prop}, (∃ (_ : a), b) ↔ a ∧ b
This theorem, `exists_prop`, states that for all propositions `a` and `b`, the existence of an instance of `b` given `a` is equivalent to the conjunction of `a` and `b`. In other words, it asserts that there exists a `b` such that `a` is true if and only if both `a` and `b` are true. This theorem is essentially a formalization of the logical rule of simplification in propositional logic.
More concisely: The theorem asserts that for all propositions `a` and `b`, `exists.prop a (exists.prop b) ↔ a ∧ b`.
|
Exists.imp
theorem Exists.imp : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∃ a, p a) → ∃ a, q a
This theorem, `Exists.imp`, states that for any sort `α` and any two properties `p` and `q` of `α`, if for every element `a` of `α`, `p a` implies `q a`, then if there exists an element `a` such that `p a` is true, there must also exist an element `a` such that `q a` is true. In simpler terms, if every element that satisfies property `p` also satisfies property `q`, then any existence of an element satisfying `p` guarantees the existence of an element satisfying `q`.
More concisely: If for all `a` in `α`, `p(a)` implies `q(a)`, then the existence of an `a` such that `p(a)` holds implies the existence of an `a` such that `q(a)` holds.
|
exists_congr
theorem exists_congr : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∃ a, p a) ↔ ∃ a, q a)
This theorem, `exists_congr`, is a statement about properties and existence in any sort (a type-like construct in Lean 4). Specifically, it says that for any sort `α`, and any two properties `p` and `q` of elements of `α`, if for every element `a` of `α`, `p` and `q` are equivalent (meaning `p a` if and only if `q a`), then the existence of an element satisfying `p` is equivalent to the existence of an element satisfying `q`. In simpler terms, if two properties are equivalent for all elements of a sort, then an element of the sort satisfies one property if and only if it satisfies the other.
More concisely: If two properties `p` and `q` are equivalent for all elements of a sort `α`, then the existence of an element of `α` satisfying `p` is equivalent to the existence of an element of `α` satisfying `q`.
|
forall₄_congr
theorem forall₄_congr :
∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4}
{p q : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop},
(∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d ↔ q a b c d) →
((∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d) ↔
∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), q a b c d)
This theorem states that for any four dependent types `α`, `β`, `γ`, and `δ`, and any two properties `p` and `q` that each take four arguments of these types respectively, if for all possible arguments `p` and `q` are logically equivalent (meaning `p` is true if and only if `q` is true), then the universal quantifications over `p` and `q` are also logically equivalent. That is, `p` holds for all combinations of arguments if and only if `q` does so as well.
More concisely: If for all dependent types `α`, `β`, `γ`, and `δ` and properties `p` and `q` taking four arguments each, `p ↔ q` implies `∀ (a: α) (b: β) (c: γ) (d: δ), p a b c d ↔ q a b c d`, then the universal quantifications over `p` and `q` are logically equivalent.
|
forall_and
theorem forall_and : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x := by
sorry
This theorem states that for any type `α` and two properties `p` and `q` defined over `α`, the statement "for every `x` of type `α`, `p x` and `q x` hold" is logically equivalent to "for every `x` of type `α`, `p x` holds and for every `x` of type `α`, `q x` holds". In other words, it says that universal quantification distributes over conjunction.
More concisely: For any type `α` and properties `p` and `q` over `α`, the statement "∀x : α, p x ∧ q x" is logically equivalent to "∀x : α, p x" ∧ "∀x : α, q x".
|
or_and_left
theorem or_and_left : ∀ {a b c : Prop}, a ∨ b ∧ c ↔ (a ∨ b) ∧ (a ∨ c)
This theorem states that the logical "OR" operation is distributive over the logical "AND" operation when "OR" is on the left. In other words, for any three propositions `a`, `b`, and `c`, the proposition "`a` OR (`b` AND `c`)" is equivalent to the proposition "(`a` OR `b`) AND (`a` OR `c`)".
More concisely: The theorem asserts that `(p ∨ (q ∧ r)) ≡ (p ∨ q) ∧ (p ∨ r)` for all propositions `p`, `q`, and `r`.
|
and_left_comm
theorem and_left_comm : ∀ {a b c : Prop}, a ∧ b ∧ c ↔ b ∧ a ∧ c
This theorem, `and_left_comm`, states that for any three propositions `a`, `b`, and `c`, the conjunction of `a`, `b`, and `c` is logically equivalent to the conjunction of `b`, `a`, and `c`. In other words, the order in which the first two propositions are arranged in this three-part conjunction does not affect the truth value of the whole statement. This essentially speaks to the commutative property of the logical "AND" operation.
More concisely: For all propositions a, b, and c, a ∧ b is logically equivalent to b ∧ a.
|
and_right_comm
theorem and_right_comm : ∀ {a b c : Prop}, (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b
This theorem, `and_right_comm`, states that for any three propositions `a`, `b`, and `c`, the proposition "(a AND b) AND c" is logically equivalent to the proposition "(a AND c) AND b". That is, within a two-level conjunction (logical AND), the right-side elements can be commutatively swapped without changing the truth value of the overall proposition.
More concisely: The theorem `and_right_comm` asserts that for all propositions a, b, and c, (a And b) And c is logically equivalent to (a And c) And b.
|
not_and'
theorem not_and' : ∀ {a b : Prop}, ¬(a ∧ b) ↔ b → ¬a
This theorem states that for any two propositions `a` and `b`, the negation of their conjunction (i.e., `¬(a ∧ b)`) is logically equivalent to the implication `b → ¬a`. In other words, the statement "not both `a` and `b` are true" is equivalent to "if `b` is true, then `a` must not be true".
More concisely: The negation of the conjunction `a ∧ b` is logically equivalent to the implication `b → ¬a`.
|
And.imp_left
theorem And.imp_left : ∀ {a b c : Prop}, (a → b) → a ∧ c → b ∧ c
This theorem, "And.imp_left", states that for any three propositional variables 'a', 'b', and 'c', if there exists a logical implication from 'a' to 'b', then it also implies that if 'a' and 'c' are true, then 'b' and 'c' will also be true. In other words, you can import the implication from 'a' to 'b' into an "and" statement with 'c', preserving the truth of 'c'.
More concisely: If `a` implies `b` in propositional logic, then `(a ∧ c)` is logically equivalent to `(b ∧ c)`.
|
exists_imp
theorem exists_imp : ∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, (∃ x, p x) → b ↔ ∀ (x : α), p x → b
This theorem, `exists_imp`, states that for any type `α`, any predicate `p` on `α`, and any proposition `b`, the proposition "There exists an `x` of type `α` such that `p x` implies `b`" is equivalent to the proposition "For all `x` of type `α`, if `p x` then `b`". In simpler terms, if having at least one `x` that satisfies `p` implies `b`, then having any `x` that satisfies `p` should also imply `b`.
More concisely: For any type `α`, predicate `p` on `α`, and proposition `b`, the proposition "there exists an `x` in `α` such that `p(x)` implies `b`" is equivalent to "for all `x` in `α`, if `p(x)` then `b`".
|
or_imp
theorem or_imp : ∀ {a b c : Prop}, a ∨ b → c ↔ (a → c) ∧ (b → c)
This theorem, named `or_imp`, states that for any three propositions `a`, `b`, and `c`, the implication that either `a` or `b` implies `c` is logically equivalent to both `a` implies `c` and `b` implies `c`. In other words, if `c` follows from either `a` or `b`, then `c` must follow from `a` and must also follow from `b`.
More concisely: The theorem `or_imp` asserts that for all propositions `a`, `b`, and `c`, `(a → c) ∧ (b → c)` is logically equivalent to `(a ∨ b) → c`.
|
and_self_iff
theorem and_self_iff : ∀ {a : Prop}, a ∧ a ↔ a
This theorem, `and_self_iff`, states that for any proposition `a`, the condition `a` and `a` is logically equivalent to just `a`. In other words, saying `a` is true and `a` is true again, is the same as simply saying `a` is true. This applies to any proposition `a`.
More concisely: For all propositions `a`, `a` is logically equivalent to `a` and `a` together.
|
and_iff_right
theorem and_iff_right : ∀ {a b : Prop}, a → (a ∧ b ↔ b)
This theorem, `and_iff_right`, states that for any two propositions `a` and `b`, if `a` is true, then the statement "`a` and `b` is true if and only if `b` is true". In other words, if we already know `a` is true, then the truth of `a ∧ b` (the conjunction of `a` and `b`) is entirely determined by the truth of `b`.
More concisely: If `a` holds, then `a` and `b` are equal in truth value to `b`.
|
exists_comm
theorem exists_comm : ∀ {α : Sort u_2} {β : Sort u_1} {p : α → β → Prop}, (∃ a b, p a b) ↔ ∃ b a, p a b
This theorem, `exists_comm`, states that for any types `α` and `β`, and for any property `p` that takes an element of `α` and an element of `β`, the existence of a pair `(a, b)` such that `p a b` holds is equivalent to the existence of a pair `(b, a)` such that `p a b` holds. In other words, the order of `a` and `b` in the existential quantification does not matter if `p a b` is true.
More concisely: For any types `α` and `β` and property `p` : `α → β → Prop`, the existence of `a : α` and `b : β` such that `p a b` holds is equivalent to the existence of `b : β` and `a : α` such that `p a b` holds.
|
Decidable.or_iff_not_imp_left
theorem Decidable.or_iff_not_imp_left : ∀ {a b : Prop} [inst : Decidable a], a ∨ b ↔ ¬a → b
This theorem, `Decidable.or_iff_not_imp_left`, states that for any propositions `a` and `b`, where `a` is a decidable proposition, the statement "`a` OR `b`" is logically equivalent to the statement "if not `a`, then `b`". This equivalence holds in classical logic. In LaTeX terms, it says that for any propositions $a$ and $b$ with $a$ being decidable, $a \lor b \iff \neg a \rightarrow b$.
More concisely: For any decidable proposition `a` and proposition `b`, `a OR b` is logically equivalent to `if not a, then b` in classical logic. (Or, in mathematical notation, `a ∨ b ↔ ¬a → b`)
|
or_self_iff
theorem or_self_iff : ∀ {a : Prop}, a ∨ a ↔ a
This theorem, `or_self_iff`, states that for any proposition `a`, the logical OR of `a` with itself is logically equivalent to `a` itself. In other words, it is saying that "either `a` is true or `a` is true" if and only if "`a` is true". This is a fundamental property of logic, and it holds universally for any proposition `a`.
More concisely: For all propositions `a`, `a \vee a` is logically equivalent to `a`.
|
Decidable.not_and_iff_or_not_not'
theorem Decidable.not_and_iff_or_not_not' : ∀ {b a : Prop} [inst : Decidable b], ¬(a ∧ b) ↔ ¬a ∨ ¬b
This theorem, `Decidable.not_and_iff_or_not_not'`, states that for any two propositions `a` and `b`, where `b` is decidable, the negation of the conjunction of `a` and `b` (`¬(a ∧ b)`) is logically equivalent to the disjunction of the negations of `a` and `b` (`¬a ∨ ¬b`). In other words, "not (a and b)" is the same as "either not a or not b".
More concisely: The negation of the conjunction of two propositions is logically equivalent to the disjunction of their negations, when one of the propositions is decidable.
|
not_or
theorem not_or : ∀ {p q : Prop}, ¬(p ∨ q) ↔ ¬p ∧ ¬q
This theorem, `not_or`, states that for all propositions `p` and `q`, the negation of the disjunction `p ∨ q` is equivalent to the conjunction of the negations `¬p ∧ ¬q`. In simpler terms, it means that "not (p or q)" is the same as "not p and not q". This is a fundamental principle in classical logic known as De Morgan's laws.
More concisely: The negation of the disjunction of propositions `p` and `q` is equivalent to the conjunction of their negations, i.e., `¬(p ∨ q) ≡ ¬p ∧ ¬q`.
|
or_iff_left
theorem or_iff_left : ∀ {b a : Prop}, ¬b → (a ∨ b ↔ a)
This theorem, `or_iff_left`, states that for any two propositions `a` and `b`, if `b` is not true (denoted by `¬b`), then the logical OR of `a` and `b` (`a ∨ b`) is equivalent to `a` itself. In other words, if `b` is false, then the truth value of the expression `a ∨ b` is determined solely by `a`, because the OR operation with a false value doesn't change the overall value of the expression.
More concisely: For all propositions `a` and `b`, `a ∨ ¬b` is equivalent to `a`.
|
and_or_left
theorem and_or_left : ∀ {a b c : Prop}, a ∧ (b ∨ c) ↔ a ∧ b ∨ a ∧ c
This theorem states that the logical "and" operation distributes over the logical "or" operation on the left side. In other words, for any three propositions `a`, `b`, and `c`, the proposition "a and (b or c)" is logically equivalent to the proposition "(a and b) or (a and c)". This is an instance of a general principle in logic and set theory known as distributivity.
More concisely: The logical "and" operation distributes over the logical "or" operation: a × (b ∨ c) ≡ (a × b) ∨ (a × c), where × represents logical and and ∨ represents logical or.
|
and_congr_right'
theorem and_congr_right' : ∀ {b c a : Prop}, (b ↔ c) → (a ∧ b ↔ a ∧ c)
This theorem, `and_congr_right'`, states that for any propositions `a`, `b`, and `c`, if `b` is logically equivalent to `c` (that is, `b` if and only if `c`), then the proposition "a and b" is logically equivalent to "a and c". Essentially, it confirms that the logical conjunction operation (i.e., "and") preserves logical equivalence on its second argument.
More concisely: If `a` is a proposition and `b` is logically equivalent to `c`, then `a ∧ b` is logically equivalent to `a ∧ c`. (Here, `∧` denotes logical conjunction.)
|
or_iff_right
theorem or_iff_right : ∀ {a b : Prop}, ¬a → (a ∨ b ↔ b)
This theorem states that for any two propositions 'a' and 'b', if 'a' is not true, then the statement 'a or b' is equivalent to 'b'. In other words, if we know that 'a' is false, then 'a or b' is true if and only if 'b' is true. This is a formalization of a basic rule of logical reasoning in propositional logic.
More concisely: If `a` is false, then `a or b` is equivalent to `b`.
|
And.imp_right
theorem And.imp_right : ∀ {a b c : Prop}, (a → b) → c ∧ a → c ∧ b
The theorem `And.imp_right` asserts that for all propositions `a`, `b`, and `c`, if there is an implication from `a` to `b`, then an implication from `c and a` to `c and b` also holds. Simply put, if we know `a` implies `b`, and we have both `c` and `a` being true, it logically follows that `c` and `b` are true.
More concisely: If `a` implies `b`, then `(c and a)` implies `(c and b)`.
|
Decidable.not_imp_comm
theorem Decidable.not_imp_comm : ∀ {a b : Prop} [inst : Decidable a] [inst : Decidable b], ¬a → b ↔ ¬b → a
This theorem states that for any two propositions `a` and `b`, given that both `a` and `b` are decidable (i.e., either `a` or `not a` is true, and similarly for `b`), the logical implication from the negation of `a` to `b` is equivalent to the logical implication from the negation of `b` to `a`. In other words, "if not `a`, then `b`" is the same as saying "if not `b`, then `a`".
More concisely: The negations of propositions `a` and `b` are logically equivalent if and only if the implication from the negation of `a` to `b` is equivalent to the implication from the negation of `b` to `a`.
|
or_and_right
theorem or_and_right : ∀ {a b c : Prop}, (a ∨ b) ∧ c ↔ a ∧ c ∨ b ∧ c
This theorem, named `or_and_right`, states the distributive property of logical conjunction (`∧`) over logical disjunction (`∨`) on the right side. In other words, for any three propositions `a`, `b`, and `c`, the statement "`a OR b` AND `c`" is logically equivalent to the statement "`a AND c` OR `b AND c`". This is a fundamental theorem in propositional logic.
More concisely: The theorem `or_and_right` asserts that for all propositions `a`, `b`, and `c`, `(a ∨ b) ∧ c` is logically equivalent to `(a ∧ c) ∨ (b ∧ c)`.
|
forall₂_congr
theorem forall₂_congr :
∀ {α : Sort u_1} {β : α → Sort u_2} {p q : (a : α) → β a → Prop},
(∀ (a : α) (b : β a), p a b ↔ q a b) → ((∀ (a : α) (b : β a), p a b) ↔ ∀ (a : α) (b : β a), q a b)
The theorem `forall₂_congr` states that for any two types `α` and `β` (where `β` is a function of `α`), given any two properties `p` and `q` that are related to `α` and `β`, if for all `a` in `α` and `b` in `β`, `p a b` is equivalent to `q a b`, then the proposition that `p a b` holds for all `a` and `b` is equivalent to the proposition that `q a b` holds for all `a` and `b`. In essence, this theorem establishes the equivalence of two universal quantifications given the equivalence of their predicates.
More concisely: If for all `a` in `α` and `b` in `β`, `p(a, b)` is equivalent to `q(a, b)`, then `∀(a : α) ∀(b : β), p(a, b)` is equivalent to `∀(a : α) ∀(b : β), q(a, b)`.
|
forall_eq
theorem forall_eq : ∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∀ (a : α), a = a' → p a) ↔ p a'
This theorem states that for any type `α`, any predicate `p` over `α`, and any element `a'` of type `α`, the statement "for all `a` in `α`, if `a` equals `a'` then `p(a)` holds" is logically equivalent to "`p(a')` holds". In other words, if `p(a)` is true whenever `a` is the same as `a'`, then `p(a')` is also true, and vice versa.
More concisely: For any type `α`, predicate `p` over `α`, and element `a'` of type `α`, the predicate `p` applied to `a'` is logically equivalent to the quantified predicate `∀a:α, a = a' → p a`.
|
forall_const
theorem forall_const : ∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], α → b ↔ b
This theorem states that for any proposition `b` and any type `α` that is nonempty (i.e., there exists at least one value of type `α`), the implication from `α` to `b` is equivalent to `b`. In other words, if we have an instance of `α` (which we know we have because `α` is nonempty), then saying "`α` implies `b`" is just the same as saying "`b`".
More concisely: For any nonempty type `α` and proposition `b`, `α → b` is provably equal to `b`.
|
dite_not
theorem dite_not :
∀ {p : Prop} {α : Sort u_1} [hn : Decidable ¬p] [h : Decidable p] (x : ¬p → α) (y : ¬¬p → α),
dite (¬p) x y = dite p (fun h => y ⋯) x
This theorem states that the negative of a proposition `P` in a `dite` (an if-then-else construct) is equivalent to swapping the branches of the construct. Specifically, for any proposition `P` and any type `α`, if `P` is decidable and its negation is also decidable, then the value of the `dite` construct when `P` is negated and the branches are swapped is the same as when `P` is not negated and the branches are not swapped. This theorem shows how logical negation interacts with the `dite` construct in Lean.
More concisely: For decidable propositions `P` and types `α`, the negation of a `dite` construct with Proposition `P` and branches `a` and `b` is equivalent to the `dite` construct with Proposition `neg P` and branches `b` and `a`.
|
exists_and_right
theorem exists_and_right : ∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, (∃ x, p x ∧ b) ↔ (∃ x, p x) ∧ b
This theorem, `exists_and_right`, states that for any type `α` and any predicate `p` of type `α → Prop` and any proposition `b`, the existence of an element of type `α` such that both `p` holds for that element and `b` is true is equivalent to the conjunction of the existence of an element of type `α` for which `p` holds and `b` being true. In other words, it equates the existence of an element satisfying a property and another independent proposition being true, with the existence of an element satisfying the property and the other proposition being true separately.
More concisely: For any type `α`, predicate `p` of type `α → Prop`, and proposition `b`, the existence of an element of type `α` satisfying `p` and `b` is equivalent to the existence of an element of type `α` satisfying `p` and the truth of `b` separately.
|
and_iff_left
theorem and_iff_left : ∀ {b a : Prop}, b → (a ∧ b ↔ a)
This theorem is stating that for all propositions `a` and `b`, if `b` is true, then `a` and `b` are equivalent to `a`. In other words, when `b` is given to be true, `a ∧ b` (the conjunction of `a` and `b`) and `a` itself express the same truth value. If `a` is true, then `a ∧ b` is also true, and vice versa.
More concisely: For all propositions `a` and `b`, if `b` is true then `a ∧ b` and `a` are equivalent.
|
forall_imp
theorem forall_imp : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∀ (a : α), p a) → ∀ (a : α), q a := by
sorry
This theorem states that for any type `α` and any two predicates `p` and `q` on `α`, if for every element `a` of `α`, `p a` implies `q a`, and if `p a` holds for all `a` in `α`, then `q a` also holds for all `a` in `α`. In the language of mathematical logic, this is the principle of modus ponens applied universally: if "`p` implies `q`" is a universal truth and `p` is universally true, then `q` must also be universally true. Here, `p` and `q` could be any properties or conditions applicable to elements of the type `α`.
More concisely: If `p` implies `q` and `p` holds for all elements of type `α`, then `q` holds for all elements of type `α`. (Modus ponens for universally quantified statements)
|
Decidable.not_iff
theorem Decidable.not_iff : ∀ {b a : Prop} [inst : Decidable b], ¬(a ↔ b) ↔ (¬a ↔ b)
This theorem states that for any two propositions `a` and `b`, where `b` is decidable, the negation of the equivalence between `a` and `b` is equivalent to the equivalence between the negation of `a` and `b`. In simpler terms, it says that if `a` is not equivalent to `b`, then this is the same as saying that `b` is equivalent to `a` being false.
More concisely: For decidable propositions `a` and `b`, `~(a ↔ b)` is equivalent to `a ↔ ~b`.
|
or_left_comm
theorem or_left_comm : ∀ {a b c : Prop}, a ∨ b ∨ c ↔ b ∨ a ∨ c
This theorem states that for any three propositions `a`, `b`, and `c`, the logical OR (`∨`) operation is left-commutative. This means that the order in which the propositions are OR'ed together does not affect the outcome: the proposition "a OR b OR c" is logically equivalent to "b OR a OR c". In other words, the result of the OR operation remains the same even when the first two propositions `a` and `b` are swapped.
More concisely: For any propositions `a`, `b`, and `c`, the logical OR `(a ∨ b ∨ c)` is equivalent to `(b ∨ a ∨ c)`.
|
not_forall_of_exists_not
theorem not_forall_of_exists_not : ∀ {α : Sort u_1} {p : α → Prop}, (∃ x, ¬p x) → ¬∀ (x : α), p x
This theorem states that for any sort `α` and any property `p` pertaining to `α`, if there exists an element of `α` for which the property `p` does not hold, then it is not the case that the property `p` holds for all elements of `α`. Put simply, if there's at least one exception, then we can't say that something is true for everything.
More concisely: If there exists an element in a sort `α` that does not have property `p`, then `p` does not hold for all elements in `α`.
|
exists₂_congr
theorem exists₂_congr :
∀ {α : Sort u_1} {β : α → Sort u_2} {p q : (a : α) → β a → Prop},
(∀ (a : α) (b : β a), p a b ↔ q a b) → ((∃ a b, p a b) ↔ ∃ a b, q a b)
This theorem, `exists₂_congr`, states that for all types `α` and `β` (where `β` is dependent on `α`), and for all predicates `p` and `q` that take two arguments (an element of `α` and an element of `β`), if for all `a` in `α` and `b` in `β a`, `p a b` is equivalent to `q a b`, then the existential quantification of `p` over both `a` and `b` is equivalent to the existential quantification of `q` over both `a` and `b`. In other words, if `p` and `q` are equivalent for all possible inputs, then there exists some `a` and `b` for which `p a b` is true if and only if there exists some `a` and `b` for which `q a b` is true.
More concisely: If for all `a` in `α` and `b` in `β(a)`, `p(a, b) ↔ q(a, b)` implies `∃(a, b). p(a, b) ↔ ∃(a, b). q(a, b)`.
|
Decidable.iff_iff_and_or_not_and_not
theorem Decidable.iff_iff_and_or_not_and_not : ∀ {a b : Prop} [inst : Decidable b], (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b := by
sorry
This theorem states that for any two propositions 'a' and 'b', given that 'b' is decidable (meaning it can definitively be proven true or false), the equivalence of 'a' and 'b' is itself equivalent to the logical disjunction (OR operation) of two conditions: 'a' and 'b' both being true, or 'a' and 'b' both being false.
More concisely: For any propositions 'a' and 'b' where 'b' is decidable, the equivalence of 'a' and 'b' is equivalent to ('a' = 'b') ≤followed by (decidable 'b') → (('a' → 'b') ∧ ('b' → 'a')) ∨ ('~'a' ∧ '~'b').
|
decide_eq_decide
theorem decide_eq_decide : ∀ {p q : Prop} {x : Decidable p} {x_1 : Decidable q}, decide p = decide q ↔ (p ↔ q) := by
sorry
The theorem `decide_eq_decide` states that for any two propositions `p` and `q`, and any two instances `x` and `x_1` of `Decidable` for `p` and `q` respectively, `decide p` is equal to `decide q` if and only if `p` is logically equivalent to `q`. This emphasizes the link between the decision procedure's results and the logical equivalence of the propositions it operates on.
More concisely: For any propositions `p` and `q`, if `Decidable p` and `Decidable q` have equivalent instances `x` and `x_1` respectively, then `decide p = decide q` if and only if `p` is logically equivalent to `q`.
|
And.imp
theorem And.imp : ∀ {a c b d : Prop}, (a → c) → (b → d) → a ∧ b → c ∧ d
This theorem, `And.imp`, states that for any four propositions `a`, `b`, `c`, and `d`, if there is a logical implication from `a` to `c` and from `b` to `d`, then if `a` and `b` are both true, it follows that `c` and `d` are also both true. In mathematical terms, this can be written as: given $(a \rightarrow c)$ and $(b \rightarrow d)$, if $a \land b$ then $c \land d$.
More concisely: If `a` implies `c` and `b` implies `d`, then `a` and `b` together imply `c` and `d` (i.e., `(a → c)` and `(b → d)` imply `(a ∧ b) → (c ∧ d)`).
|
Decidable.not_and_iff_or_not_not
theorem Decidable.not_and_iff_or_not_not : ∀ {a b : Prop} [inst : Decidable a], ¬(a ∧ b) ↔ ¬a ∨ ¬b
This theorem, `Decidable.not_and_iff_or_not_not`, states the relationship between logical negation, conjunction, and disjunction properties for any given propositions `a` and `b`. Specifically, it declares that not both `a` and `b` being true is equivalent to either `a` is not true or `b` is not true. This is applicable when `a` is a decidable proposition. The theorem codifies a basic law of logic, known as De Morgan's laws.
More concisely: The theorem `Decidable.not_and_iff_or_not` in Lean 4 states that for any decidable propositions `a` and `b`, `~(a ∧ b)` is equivalent to `(~a) ∨ (~b)`.
|
exists_or
theorem exists_or : ∀ {α : Sort u_1} {p q : α → Prop}, (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x
This theorem states that for any type `α` and for any properties `p` and `q` on `α`, the existence of an element in `α` that satisfies either `p` or `q` is logically equivalent to the existence of an element in `α` that satisfies `p` or the existence of an element in `α` that satisfies `q`. In mathematical terms, it means that ∃x (p(x) ∨ q(x)) is equivalent to (∃x p(x)) ∨ (∃x q(x)).
More concisely: The theorem asserts that for any type `α` and properties `p` and `q` on `α`, the existence of an element in `α` satisfying `p` or `q` is logically equivalent to the existence of an element in `α` satisfying `p` or an independent element satisfying `q`. (Note: In the original statement, "or the existence of an element in `α` that satisfies `q`" seems to be redundant as it is already stated that the property holds for either `p` or `q`.)
|
Decidable.not_not
theorem Decidable.not_not : ∀ {p : Prop} [inst : Decidable p], ¬¬p ↔ p
This theorem, `Decidable.not_not`, states that for any proposition `p` that can be decided (i.e., either `p` is true or `p` is false), the double negation of `p` is logically equivalent to `p` itself. In other words, if we know that it is not the case that `p` is not true (¬¬p), then we can conclude that `p` must be true, and vice versa. This theorem is a formal statement in Lean of a fundamental principle of classical logic, namely the law of double negation.
More concisely: The double negation of a decidable proposition is logically equivalent to the proposition itself.
|
and_or_right
theorem and_or_right : ∀ {a b c : Prop}, a ∧ b ∨ c ↔ (a ∨ c) ∧ (b ∨ c)
This theorem states that the logical "or" operation distributes over the logical "and" operation on its right-hand side. In particular, for any three propositions `a`, `b`, and `c`, the proposition "`a` and `b`, or `c`" is logically equivalent to the proposition "(`a` or `c`) and (`b` or `c`)".
More concisely: The logical "and" of the propositions `a` and `b`, and the proposition `c`, is logically equivalent to the proposition (`a` or `c`) and (`b` or `c`).
|
and_congr
theorem and_congr : ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∧ b ↔ c ∧ d)
This theorem, `and_congr`, states that for any four propositional variables `a`, `b`, `c`, and `d`, if `a` is logically equivalent to `c` and `b` is logically equivalent to `d`, then the logical conjunction (AND operation) of `a` and `b` is also logically equivalent to the logical conjunction of `c` and `d`. In mathematical terms, if $a \Leftrightarrow c$ and $b \Leftrightarrow d$, then $(a \land b) \Leftrightarrow (c \land d)$.
More concisely: If $a$ is logically equivalent to $c$ and $b$ is logically equivalent to $d$, then $(a \land b) \Leftrightarrow (c \land d)$.
|
forall₅_congr
theorem forall₅_congr :
∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4}
{ε : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Sort u_5}
{p q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop},
(∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e ↔ q a b c d e) →
((∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e) ↔
∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), q a b c d e)
This theorem, `forall₅_congr`, states that for every five nested dependent types `α`, `β`, `γ`, `δ`, and `ε`, and two predicate functions `p` and `q` that depend on these five types, if for all possible parameters, `p` is logically equivalent to `q` (`p` if and only if `q`), then the universal quantification over `p` is logically equivalent to the universal quantification over `q`. In simpler terms, if two predicates are true under the same conditions for all possible values of five nested dependent types, then the statement "all values satisfy `p`" is true if and only if "all values satisfy `q`".
More concisely: If for all dependent types α, β, γ, δ, and ε, and predicate functions p and q, p(α, β, γ, δ, ε) is logically equivalent to q(α, β, γ, δ, ε) for all parameters, then ∀x, p(x) is logically equivalent to ∀x, q(x).
|
Decidable.not_imp_symm
theorem Decidable.not_imp_symm : ∀ {a b : Prop} [inst : Decidable a], (¬a → b) → ¬b → a
This theorem states that for any two propositions `a` and `b`, where `a` is decidable, if we have a function from the negation of `a` to `b`, and the negation of `b` holds, then `a` must be true. Essentially, it is stating that if `a` being false implies `b`, and `b` is false, then `a` must be true, which is a form of contraposition in logic.
More concisely: If `a` is decidable and there exists a function from ∼`a` to `b` when ∼`b` holds, then `a` is true. (This is a form of contrapositive of the conditional `a → b` in logic, where `→` denotes material implication.)
|
decide_eq_true_iff
theorem decide_eq_true_iff : ∀ (p : Prop) [inst : Decidable p], decide p = true ↔ p
This theorem states that for any proposition `p` and given that `p` is decidable (i.e., there exists a proof that `p` is either true or false), the `decide` function on `p` equals `true` if and only if `p` is true. In other words, the `decide` function accurately reflects the truth value of `p` – it returns `true` when `p` is true, and something other than `true` when `p` is not true.
More concisely: For any decidable proposition `p` in Lean, `decide p = tt` if and only if `p` is true.
|
forall_congr'
theorem forall_congr' :
∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∀ (a : α), p a) ↔ ∀ (a : α), q a)
This theorem states that for all types `α` and any two properties `p` and `q` that can be applied to elements of `α`, if for every element `a` of type `α`, the property `p a` is equivalent to the property `q a`, then the statement "for all `a` of type `α`, `p a` holds" is equivalent to "for all `a` of type `α`, `q a` holds". In simpler words, if two properties are equivalent for all elements of a certain type, then any statement about all elements of that type having one property is equivalent to the same statement with the other property.
More concisely: If for all `α` and properties `p` and `q` on `α`, `p a ↔ q a` for all `a : α` implies `∀ a, p a ↔ ∀ a, q a`.
|
Decidable.imp_iff_not_or
theorem Decidable.imp_iff_not_or : ∀ {a b : Prop} [inst : Decidable a], a → b ↔ ¬a ∨ b
This theorem states that, for any propositions `a` and `b`, and given that `a` is decidable (meaning we can definitively say whether `a` is true or false), the implication `a → b` (if `a` then `b`) is logically equivalent to `¬a ∨ b` (either `a` is not true, or `b` is true). In other words, an implication holds true either when its antecedent is false or when its consequent is true.
More concisely: For any propositions `a` and `b`, `a → b` is logically equivalent to `¬a ∨ b`.
|