true_implies
theorem true_implies : ∀ (p : Prop), (True → p) = p
This theorem, named `true_implies`, states that for any proposition `p`, the implication of `True` leading to `p` is equivalent to `p` itself. In other words, if `p` is a logical proposition, then `True → p` (which reads "True implies `p`") is the same as `p`. This is a natural result in logic, since if we know that `True` implies `p`, then `p` must be `True`, and vice versa.
More concisely: For any proposition `p` in Lean, `True → p` is logically equivalent to `p`.
|
eq_self
theorem eq_self : ∀ {α : Sort u_1} (a : α), (a = a) = True
This theorem, `eq_self`, states that for any element `a` of any sort `α`, the proposition that `a` equals itself is true. This is a universal truth in mathematics, often referred to as the reflexivity of equality, which asserts that each element is equal to itself. The theorem applies to any sort in Lean, which could be either types or propositions.
More concisely: For all elements `a` of any type `α` in Lean, `a` equals `a`.
|
Bool.and_false
theorem Bool.and_false : ∀ (b : Bool), (b && false) = false
This theorem states that for any boolean value `b`, the logical AND between this boolean `b` and `false` is always `false`. By the definition of logical AND, this result is true because the AND operation between any value and `false` always results in `false`.
More concisely: For any boolean value `b`, `b` and `false` logically AND-ed together equal `false`.
|
or_self
theorem or_self : ∀ (p : Prop), (p ∨ p) = p
This theorem states that for any proposition `p`, the logical disjunction of `p` and `p` is equivalent to `p` itself. In other words, in terms of classical logic, if you say "Either `p` is true, or `p` is true," you are essentially just saying "`p` is true". This is a fundamental property of the "or" operator in logic.
More concisely: For any proposition `p` in Lean, `p` or `p` is logically equivalent to `p`.
|
Bool.not_eq_true
theorem Bool.not_eq_true : ∀ (b : Bool), (¬b = true) = (b = false)
This theorem states that for any boolean value `b`, the statement "not `b` is equal to true" is equivalent to the statement "`b` is equal to false". In other words, negating a boolean value and equating it to true gives the same result as directly equating the original boolean value to false.
More concisely: The negation of a boolean value `b` is equivalent to `false`, or equivalently, `not b` is equal to `false`.
|
Nat.le_zero_eq
theorem Nat.le_zero_eq : ∀ (a : ℕ), (a ≤ 0) = (a = 0)
This theorem states that for any natural number 'a', 'a' is less than or equal to zero if and only if 'a' equals zero. In other words, for the set of natural numbers, the only way a number can satisfy the condition of being less than or equal to zero is if it is zero itself.
More concisely: For any natural number 'a', a = 0 if and only if a ≤ 0.
|
true_and
theorem true_and : ∀ (p : Prop), (True ∧ p) = p
This theorem states that for any proposition 'p', the logical conjunction of 'True' and 'p' is equivalent to 'p'. In other words, 'True' combined with any proposition using the logical operator 'and' does not change the truth value of that proposition. This theorem reflects the identity law in propositional logic.
More concisely: For any proposition p in Lean, True and p are logically equivalent.
|
and_imp
theorem and_imp : ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → c
This theorem, `and_imp`, is a statement about logical implications in propositional logic. It asserts that for any propositions `a`, `b`, and `c`, the implication from the conjunction of `a` and `b` to `c` is logically equivalent to the double implication from `a` to `b` to `c`. In other words, if `a` and `b` together imply `c`, then it's the same as saying if `a` is true, then if `b` is true, `c` is also true.
More concisely: The theorem `and_imp` asserts that for all propositions `a`, `b`, and `c`, `(a ∧ b) → c` is logically equivalent to `a → (b → c)`.
|
and_iff_left_of_imp
theorem and_iff_left_of_imp : ∀ {a b : Prop}, (a → b) → (a ∧ b ↔ a)
This theorem states that for any two propositions `a` and `b`, if `a` implies `b` (written as `a → b`), then `a ∧ b` is logically equivalent to `a`. In other words, if `a` being true always leads to `b` being true, then the statement "`a` and `b` are both true" is the same as just "`a` is true".
More concisely: If `a` implies `b`, then `a ∧ b` is logically equivalent to `a`. (Or, `a → b` implies `a ∧ b ≡ a`.)
|
Bool.true_or
theorem Bool.true_or : ∀ (b : Bool), (true || b) = true
This theorem states that for any Boolean value `b`, the logical OR operation between `true` and `b` is always `true`. In other words, no matter what `b` is, if one of the arguments is `true`, the result of `true OR b` is always `true`. This corresponds to the general law of Boolean algebra that `true OR anything` is `true`.
More concisely: For all Boolean values `b`, `true` or `b` is equal to `true`.
|
and_iff_right_iff_imp
theorem and_iff_right_iff_imp : ∀ {a b : Prop}, (a ∧ b ↔ b) ↔ b → a
This theorem, `and_iff_right_iff_imp`, states that for any two propositions `a` and `b`, the statement "`a` and `b` is equivalent to `b`" is equivalent to "`b` implies `a`". In other words, if the truth of `b` is enough to guarantee both `a` and `b` are true, then `b` being true implies `a` is true.
More concisely: The theorem `and_iff_right_iff_imp` in Lean 4 states that for all propositions `a` and `b`, `(a ∧ b) ↔ b ⟹ a`.
|
and_assoc
theorem and_assoc : ∀ {a b c : Prop}, (a ∧ b) ∧ c ↔ a ∧ b ∧ c
This theorem, `and_assoc`, states that for any three propositions `a`, `b`, and `c`, the logical 'and' operation (`∧`) is associative. In other words, the proposition "(a and b) and c" is logically equivalent to the proposition "a and (b and c)". This means if you know that "a and b" is true and "c" is also true, it's the same as knowing "a" is true and "b and c" is true. These two forms are interchangeable.
More concisely: The logical 'and' operation is associative: (a ∧ b) ∧ c ≡ a ∧ (b ∧ c) for all propositions a, b, and c.
|
and_congr_right
theorem and_congr_right : ∀ {a b c : Prop}, (a → (b ↔ c)) → (a ∧ b ↔ a ∧ c)
This theorem, `and_congr_right`, states that for any three propositions `a`, `b`, and `c`, if it is true that `a` implies an equivalence between `b` and `c`, then there's an equivalence between `a ∧ b` and `a ∧ c`. In other words, if `a` being true allows us to say `b` if and only if `c`, then the conjunction of `a` and `b` is equivalent to the conjunction of `a` and `c`.
More concisely: If `a` implies `b ↔ c`, then `a ∧ b ≡ a ∧ c`.
|
false_and
theorem false_and : ∀ (p : Prop), (False ∧ p) = False
This theorem states that for any proposition `p`, the logical conjunction (i.e., "and") of `False` and `p` is always `False`. This is due to the property of logical conjunctions where if any of the propositions is `False`, the whole conjunction is `False` regardless of the truth value of the other propositions.
More concisely: The logical conjunction of False and any proposition p is equal to False.
|
and_iff_left_iff_imp
theorem and_iff_left_iff_imp : ∀ {a b : Prop}, (a ∧ b ↔ a) ↔ a → b
This theorem states that for any two propositions `a` and `b`, the equivalence of `a ∧ b` (the conjunction of `a` and `b`) and `a` is itself equivalent to the implication from `a` to `b` (i.e., if `a` is true, then `b` must also be true). The intuition behind this is that if `a` and `b` together are equivalent to `a` alone, then `a` being true is enough to guarantee that `b` is also true.
More concisely: The theorem asserts that for all propositions `a` and `b`, the equivalence of `a ∧ b` and `a` is equivalent to the implication `a → b`.
|
ite_cond_eq_false
theorem ite_cond_eq_false :
∀ {α : Sort u} {c : Prop} {x : Decidable c} (a b : α), c = False → (if c then a else b) = b
This theorem, `ite_cond_eq_false`, states that for any type `α` and propositions `c` and `x`, where `x` can decide `c`, and any two instances `a` and `b` of `α`, if `c` is equivalent to `False`, then the "if-then-else" expression `(if c then a else b)` will always result in `b`. In other words, if the condition in an "if-then-else" clause is False, then the part following "else" will always be executed.
More concisely: If `c` is equivalent to `False` and `x` decides `c`, then `(if c then a else b)` equals `b` for all `α`, `a`, and `b` of type `α`.
|
decide_eq_true_eq
theorem decide_eq_true_eq : ∀ {p : Prop} [inst : Decidable p], (decide p = true) = p
This theorem states that for any proposition `p` and `x`, which is a decidable instance of `p`, the result of applying the `decide` function to `p` being `true` is equivalent to the proposition `p` itself being true. In other words, it formalizes the intuitive idea that if a proposition is decidable, deciding it and getting `true` means that the proposition is itself true.
More concisely: For any decidable proposition `p` and instance `x`, `decide p x = some true` if and only if `p x` holds.
|
Bool.or_false
theorem Bool.or_false : ∀ (b : Bool), (b || false) = b
This theorem states that for all boolean values `b`, the boolean OR operation (`||`) of `b` and `false` is equal to `b`. In other words, it asserts that the identity element for the boolean OR operation is `false`, since combining any boolean value with `false` using boolean OR yields the original boolean value.
More concisely: For all boolean values `b`, `b || false = b`.
|
Bool.not_false
theorem Bool.not_false : (!false) = true
This theorem states that the logical negation of "false" (`!false`), in Boolean logic, is "true". It mirrors the standard truth table for logical NOT, where NOT false equals true. In simpler terms, it's a formal expression of the fact that if something is not false, then it must be true.
More concisely: The logical negation of false is true. (`!false = true`)
|
and_congr_left
theorem and_congr_left : ∀ {c a b : Prop}, (c → (a ↔ b)) → (a ∧ c ↔ b ∧ c)
This theorem, `and_congr_left`, states that for any three propositions `a`, `b`, and `c`, if it holds that `c` implies the equivalence of `a` and `b`, then it follows that the conjunction of `a` and `c` is equivalent to the conjunction of `b` and `c`. In mathematical terms, for all propositions `a`, `b`, `c`, if (`c` implies `a` is equivalent to `b`), then (`a` and `c` is equivalent to `b` and `c`).
More concisely: If `c` implies `a ≤f/= b`, then `a and c ≤f/= b and c`.
|
and_iff_right_of_imp
theorem and_iff_right_of_imp : ∀ {b a : Prop}, (b → a) → (a ∧ b ↔ b)
This theorem, `and_iff_right_of_imp`, states that for any two propositions `a` and `b`, if `b` implies `a`, then `a ∧ b` is equivalent to `b`. In other words, if `b` being true guarantees the truth of `a`, then the conjunction `a ∧ b` is true if and only if `b` is true.
More concisely: If `b` implies `a`, then `a ∧ b` is equivalent to `b`.
|
implies_true
theorem implies_true : ∀ (α : Sort u), (α → True) = True
This theorem, named `implies_true`, states that for any type or sort `α`, the proposition that `α` implies `True` is always `True`. In other words, it asserts that if you have a statement of the form "`α` implies `True`", that statement itself is always true, regardless of what `α` might be. Using the language of predicate logic, this corresponds to the tautology that "`α` implies `True`" is always `True`.
More concisely: For any type or sort `α`, the proposition `α → True` is true. (In predicate logic, this is the tautology `∀α, α → True`.)
|
ne_eq
theorem ne_eq : ∀ {α : Sort u_1} (a b : α), (a ≠ b) = ¬a = b
This theorem, `ne_eq`, states that for all types `α` and for any two elements `a` and `b` of that type, the assertion that `a` is not equal to `b` (`a ≠ b`) is equivalent to the negation of the assertion that `a` is equal to `b` (`¬a = b`). In other words, it formally encodes the intuitive notion that saying "A is not equal to B" is the same as saying "It is not the case that A is equal to B".
More concisely: The theorem `ne_eq` asserts that for all types `α` and elements `a` and `b` of type `α`, the propositions `a ≠ b` and `¬a = b` are logically equivalent.
|
Eq.mpr_prop
theorem Eq.mpr_prop : ∀ {p q : Prop}, p = q → q → p
This theorem, `Eq.mpr_prop`, states that for any two propositions `p` and `q`, if `p` is equal to `q` and `q` is true, then `p` is also true. It applies the principle of substitutability of identicals in a logical context, asserting the transferability of truth values between equivalent propositions.
More concisely: If two propositions are equal and one is true, then the other is also true.
|
heq_eq_eq
theorem heq_eq_eq : ∀ {α : Sort u_1} (a b : α), HEq a b = (a = b)
This theorem, `heq_eq_eq`, asserts that for any type, denoted by `α`, and any two elements `a` and `b` of that type, the heterogeneous equality (`HEq`) of `a` and `b` is the same as the standard equality (`=`) of `a` and `b`. In other words, `HEq a b` and `a = b` are interchangeable for any given `a` and `b` of the same type `α`.
More concisely: For any type `α` and elements `a` and `b` of type `α`, the heterogeneous equality `HEq a b` is equivalent to the standard equality `a = b`.
|
eq_true_of_decide
theorem eq_true_of_decide : ∀ {p : Prop} [inst : Decidable p], decide p = true → p = True
This theorem, `eq_true_of_decide`, states that for any proposition `p` and any instance `x` of `Decidable p` (i.e., `p` is a decidable proposition), if the `decide` function returns `true` when applied to `p`, then `p` must be equivalent to `True`. In other words, if our decision-making process declares `p` to be `true`, then `p` is indeed a true proposition.
More concisely: If `p` is a decidable proposition and `decide p` returns `true`, then `p ≡ True`.
|
or_assoc
theorem or_assoc : ∀ {a b c : Prop}, (a ∨ b) ∨ c ↔ a ∨ b ∨ c
This theorem, `or_assoc`, states that for any three propositions `a`, `b`, and `c`, the logical OR (`∨`) operation is associative. In other words, the proposition "`(a OR b) OR c`" is logically equivalent to "`a OR (b OR c)`". This means that the parentheses can be moved without changing the truth value of the entire expression.
More concisely: The logical OR operation is associative, that is, `(a ∨ b) ∨ c` is equivalent to `a ∨ (b ∨ c)` for any propositions `a`, `b`, and `c`.
|
or_true
theorem or_true : ∀ (p : Prop), (p ∨ True) = True
This theorem states that for any proposition 'p', the logical disjunction (denoted by '∨') of 'p' and 'True' is always 'True'. In other words, regardless of whether 'p' is true or false, since one of the components of the disjunction is 'True', the overall outcome will always be 'True'. This aligns with the rules of Boolean logic where anything OR'd with 'True' results in 'True'.
More concisely: For any proposition p, p ∨ True is true.
|
iff_congr
theorem iff_congr : ∀ {p₁ p₂ q₁ q₂ : Prop}, (p₁ ↔ p₂) → (q₁ ↔ q₂) → ((p₁ ↔ q₁) ↔ (p₂ ↔ q₂))
This theorem, `iff_congr`, states that for any four propositions: `p₁`, `p₂`, `q₁`, `q₂`, if `p₁` is logically equivalent to `p₂`, and `q₁` is logically equivalent to `q₂`, then the logical equivalence between `p₁` and `q₁` is also logically equivalent to the logical equivalence between `p₂` and `q₂`. In mathematical terms, if \( p₁ ⇔ p₂ \) and \( q₁ ⇔ q₂ \), then \( (p₁ ⇔ q₁) ⇔ (p₂ ⇔ q₂) \).
More concisely: If `p₁ ⇔ p₂` and `q₁ ⇔ q₂`, then `(p₁ ⇔ q₁) ⇔ (p₂ ⇔ q₂)`. In other words, the logical equivalence relation is transitive on propositions.
|
beq_self_eq_true
theorem beq_self_eq_true : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α), (a == a) = true
This theorem, named `beq_self_eq_true`, states that for any type `α`, given that `α` has a binary equality (`BEq`) instance and obeys the laws of binary equality (`LawfulBEq`), the binary equality of any element `a` of type `α` with itself is true. Essentially, it is confirming that binary equality is reflexive, i.e., for all `a` of type `α`, `a` is equal to `a`.
More concisely: For any type `α` with reflexive binary equality `BEq`, `a BEq a` holds for all `a : α`.
|
eq_false_of_decide
theorem eq_false_of_decide : ∀ {p : Prop} {x : Decidable p}, decide p = false → p = False
This theorem states that for all propositions `p` and any instance `x` of `p` being decidable, if the decision procedure `decide p` returns `false`, then the proposition `p` is equivalent to `False`. It essentially indicates that if a decidable proposition is determined to be false, then the proposition itself is false. This is used in the context where the truth value of a proposition can be algorithmically determined.
More concisely: If a decidable proposition `p` returns `false` when applied to an instance `x`, then `p` is equivalent to `False`.
|
Bool.not_not
theorem Bool.not_not : ∀ (b : Bool), (!!b) = b
This theorem, `Bool.not_not`, states that for all boolean values `b`, applying the boolean negation operator twice (`!!b`) will yield the original boolean value `b`. This is equivalent to saying that double negation in boolean logic returns the original value, which is a standard principle in classical logic.
More concisely: For all booleans `b`, `!!b` equals `b`.
|
or_iff_left_of_imp
theorem or_iff_left_of_imp : ∀ {b a : Prop}, (b → a) → (a ∨ b ↔ a)
This theorem, `or_iff_left_of_imp`, states that for any two propositions `a` and `b`, if it is the case that `b` implies `a` (`b → a`), then the proposition `a ∨ b` is equivalent to `a` (`a ∨ b ↔ a`). In other words, if `b` being true necessarily means `a` is true, then `a` being true or `b` being true is the same as just `a` being true.
More concisely: If `b` implies `a`, then `a` is logically equivalent to `a` or `b`. (`(b → a)` implies `(a ↔ a ∨ b)`)
|
false_iff
theorem false_iff : ∀ (p : Prop), (False ↔ p) = ¬p
This theorem, `false_iff`, states that for all propositions `p`, the statement (False is equivalent to `p`) is equivalent to the negation of `p`. In other words, if `p` is equivalent to `False`, then `p` should be false, i.e., `¬p` should be true.
More concisely: The theorem `false_iff` asserts that for all propositions `p`, `False` is equivalent to the negation of `p`, i.e., `False ≡ ¬p`.
|
dite_congr
theorem dite_congr :
∀ {b c : Prop} {α : Sort u_1} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α}
{v : ¬c → α} (h₁ : b = c), (∀ (h : c), x_1 ⋯ = u h) → (∀ (h : ¬c), y ⋯ = v h) → dite b x_1 y = dite c u v
This theorem, `dite_congr`, states that for any propositions `b` and `c`, a sort `α`, a decidable `b` denoted by `x`, a decidable `c` denoted by `inst`, functions `x_1 : b → α`, `u : c → α`, `y : ¬b → α`, `v : ¬c → α`, if `b` is equal to `c` (expressed by `h₁ : b = c`), and if for all `c`, `x_1` equals `u`, and for all `¬c`, `y` equals `v`, then the application of `dite` (if then else construct) on `b`, `x_1`, `y` equals the application of `dite` on `c`, `u`, `v`. In other words, under these conditions, the 'if-then-else' evaluations of `b` and `c` will be equivalent.
More concisely: Given decidable propositions `b` and `c`, functions `x_1 : b → α`, `u : c → α`, `y : ¬b → α`, `v : ¬c → α`, and if `b = c`, `x_1 = u` on `c` and `y = v` on `¬c`, then `dite b x_1 y` = `dite c u v`.
|
Bool.true_and
theorem Bool.true_and : ∀ (b : Bool), (true && b) = b
This theorem states that for all Boolean values `b`, the logical "and" operation (represented by `&&`) between `true` and `b` is equal to `b` itself. In other words, `true` combined with any Boolean value `b` using the "and" operation will always yield `b`. This is a basic property of Boolean algebra.
More concisely: For all Boolean values `b`, `true && b = b`.
|
not_and
theorem not_and : ∀ {a b : Prop}, ¬(a ∧ b) ↔ a → ¬b
This theorem, `not_and`, expresses a logical equivalence in the domain of propositional logic. It states that for any two propositions `a` and `b`, the negation of the conjunction `a ∧ b` (not both `a` and `b` are true at the same time) is logically equivalent to the assertion that if `a` is true, then `b` must not be true (`a` implies not `b`). This theorem can be used to transform expressions in propositional logic, and it is a fundamental result regarding the relationship between conjunction and negation.
More concisely: The negation of the conjunction `a ∧ b` is logically equivalent to `a → ¬b`.
|
dite_cond_eq_true
theorem dite_cond_eq_true :
∀ {α : Sort u} {c : Prop} {x : Decidable c} {t : c → α} {e : ¬c → α} (h : c = True), dite c t e = t ⋯
This theorem states that for any type `α`, proposition `c`, decidable instance `x` of `c`, function `t` from `c` to `α`, and function `e` from the negation of `c` to `α`, if `c` is equal to `True`, then the expression `dite c t e`, which chooses between `t` and `e` based on the truth of `c`, is equal to `t`. In other words, when the condition `c` is true, `dite` expression will select the first function `t`.
More concisely: For any decidable proposition `c` of type `Prop`, function `t : c → α`, and function `e : ¬c → α`, if `c` holds, then `dite c t e = t`.
|
iff_false
theorem iff_false : ∀ (p : Prop), (p ↔ False) = ¬p
This theorem states that for any proposition `p`, the bi-conditional `p ↔ False` is equivalent to the negation of `p`, denoted as `¬p`. In other words, saying that `p` is logically equivalent to `False` is the same as saying `p` is not true.
More concisely: The theorem asserts that for any proposition `p`, the bi-conditional `p ↔ False` is equivalent to the negation `¬p` in Lean logic.
|
implies_congr_ctx
theorem implies_congr_ctx : ∀ {p₁ p₂ q₁ q₂ : Prop}, p₁ = p₂ → (p₂ → q₁ = q₂) → (p₁ → q₁) = (p₂ → q₂)
This theorem, `implies_congr_ctx`, states that for any four propositions `p₁`, `p₂`, `q₁`, and `q₂`, if `p₁` is equal to `p₂` and, within the context where `p₂` is true, `q₁` is equal to `q₂`, then the implication `p₁ → q₁` is equivalent to `p₂ → q₂`. Essentially, it establishes that if we change the antecedent and consequent of an implication in a congruent way, the overall truth of the implications remains the same.
More concisely: If `p₁ = p₂` and `(p₂ ⊢ q₁ = q₂)`, then `(p₁ → q₁) = (p₂ → q₂)`. (In Lean's type theory, `⊢` represents the context in which a judgment is being made.)
|
Or.imp_right
theorem Or.imp_right : ∀ {b c a : Prop}, (b → c) → a ∨ b → a ∨ c
This theorem, `Or.imp_right`, states that for any three propositions `a`, `b`, and `c`, if we have a hypothetical implication from `b` to `c`, then an implication from the logical disjunction `a ∨ b` to `a ∨ c` is guaranteed. In other words, if we know that `b` implies `c`, and if we have either `a` or `b`, then we can assert that we have either `a` or `c`.
More concisely: If `b` implies `c`, then `a ∨ b` implies `a ∨ c` in Lean.
|
and_true
theorem and_true : ∀ (p : Prop), (p ∧ True) = p
This theorem, `and_true`, is stating that for all propositions `p`, the logical conjunction of `p` and `True` is equivalent to `p` itself. In other words, if you have a statement `p` and you add "and true" to it, it doesn't change the truth value of the original statement `p`. This statement is a basic property of logical conjunction in classical logic.
More concisely: For all propositions p, p ∧ True is equivalent to p. (In classical logic, conjunction with a true proposition does not change the truth value of the original proposition.)
|
implies_congr
theorem implies_congr : ∀ {p₁ p₂ : Sort u} {q₁ q₂ : Sort v}, p₁ = p₂ → q₁ = q₂ → (p₁ → q₁) = (p₂ → q₂)
This theorem, `implies_congr`, states that for any two pairs of "Sorts" (`p₁, p₂` of type `Sort u` and `q₁, q₂` of type `Sort v`), if `p₁` equals `p₂` and likewise `q₁` equals `q₂`, then the implication (or function) from `p₁` to `q₁` is equal to the implication from `p₂` to `q₂`. In simpler terms, if we have two identical pairs, then the function that maps the elements of the first pair is the same as the function that maps the elements of the second pair.
More concisely: If two functions have the same domain and codomain and their domains are equal, then they are equal as functions.
|
and_congr_right_iff
theorem and_congr_right_iff : ∀ {a b c : Prop}, (a ∧ b ↔ a ∧ c) ↔ a → (b ↔ c)
This theorem states that for any three propositions `a`, `b`, and `c`, the equivalence of "a and b" with "a and c" is equivalent to the implication that if `a` is true, then `b` is equivalent to `c`. In other words, if we know `a` to be true, then the conditions `b` and `c` are interchangeable in an "and" relationship with `a`.
More concisely: The theorem asserts that for propositions `a`, `b`, and `c`, `(a ↔ b) ↔ (a ↔ c) ↔ (a → b ↔ c)`.
|
ite_self
theorem ite_self : ∀ {α : Sort u} {c : Prop} {d : Decidable c} (a : α), (if c then a else a) = a
This theorem, denoted as `ite_self`, states that for any type `α`, any proposition `c`, any decidable condition `d` derived from `c`, and any element `a` of type `α`, the result of the 'if-then-else' operation (`if c then a else a`) is always equal to `a` itself, regardless of whether condition `c` is true or false. In simpler terms, if the two outcomes of an 'if-then-else' operation are the same, then the operation is equivalent to that outcome.
More concisely: For any type `α`, proposition `c` over `α`, decidable `d` derived from `c`, and `a` : `α`, `if c then a else a` equals `a`.
|
ite_congr
theorem ite_congr :
∀ {α : Sort u_1} {b c : Prop} {x y u v : α} {s : Decidable b} [inst : Decidable c],
b = c → (c → x = u) → (¬c → y = v) → (if b then x else y) = if c then u else v
This theorem, `ite_congr`, states that for any type `α`, propositions `b` and `c`, and elements `x`, `y`, `u`, `v` of type `α`, given that we can decide whether `b` and `c` are true or false, if `b` is equal to `c`, and if when `c` is true `x` equals `u` and when `c` is false `y` equals `v`, then the value of the if-then-else expression `if b then x else y` is equal to the value of the if-then-else expression `if c then u else v`. In simpler terms, this theorem is about the congruency of if-then-else expressions under certain conditions.
More concisely: If `b` is equal to `c`, and for all elements `x`, `y`, `u`, `v` of type `α`, `x = u` when `c` is true and `y = v` when `c` is false, then `if b then x else y` is equal to `if c then u else v`.
|
decide_not
theorem decide_not : ∀ {p : Prop} [g : Decidable p] [h : Decidable ¬p], (decide ¬p) = !decide p
This is a theorem about propositions and decision procedures in Lean. It states that for any given proposition `p` and a decision procedure `h` for `p`, the decision for the negation of `p` (`¬p`) is equivalent to the negation of the decision for `p`. This means that if `p` is decided to be true, then `¬p` is decided to be false, and vice versa.
More concisely: For any proposition `p` and decision procedure `h`, if `h(p)` holds then `h(¬p)` does not hold, and conversely.
|
true_iff
theorem true_iff : ∀ (p : Prop), (True ↔ p) = p
This theorem states that, for any given proposition `p`, the bi-conditional statement (indicated by `↔`) between the truth value `True` and `p` is equivalent to `p` itself. In other words, the equivalence of `p` and `True` is the same as stating `p` itself. More formally, this can be expressed as: If `p` is true, then `True` is equivalent to `p`, and if `p` is false, then `True` is not equivalent to `p`.
More concisely: For all propositions `p`, `p ↔ True` is equivalent to `p`.
|
false_implies
theorem false_implies : ∀ (p : Prop), (False → p) = True
This theorem states that for any proposition 'p', the implication of 'False' leading to 'p' is always 'True'. In mathematical terms, it asserts that any statement can be derived from a contradiction. This is a standard principle known as "ex falso sequitur quodlibet" or 'from falsehood, anything follows'.
More concisely: The theorem asserts that for any proposition 'p' in Lean, ⊥ → p holds, where ⊥ represents the logical falsity. In other words, anything can be derived from a contradiction.
|
iff_self
theorem iff_self : ∀ (p : Prop), (p ↔ p) = True
This theorem, named 'iff_self', states that for any proposition 'p', the logical biconditional (if and only if) of 'p' with itself is always true. In other words, the theorem asserts that any proposition is equivalent to itself.
More concisely: For any proposition p, p iff p holds true.
|
Init.SimpLemmas._auxLemma.1
theorem Init.SimpLemmas._auxLemma.1 : ∀ {α β : Sort u} (h : α = β) (a : α), HEq (cast h a) a = True
This theorem, named `Init.SimpLemmas._auxLemma.1`, states that for any proposition `a`, the conjunction of `a` and its negation (i.e., `a` and `not a`) is equivalent to `False`. In other words, it is impossible for a proposition and its negation to both be true at the same time. This is a fundamental principle in classical logic known as the law of non-contradiction.
More concisely: In classical logic, the conjunction of a proposition and its negation equals False.
|
iff_true
theorem iff_true : ∀ (p : Prop), (p ↔ True) = p
This theorem states that for any proposition `p`, the equivalence of `p` and `True` is the same as `p` itself. In other words, it asserts that if we have a logical equivalence (represented by the ↔ symbol) between any proposition and the truth value `True`, this is logically identical to the original proposition `p`. This is consistent with the intuitive understanding of truth in logic, since any statement that is equivalent to `True` must be true itself.
More concisely: For any proposition `p` in Lean, `p ↔ True` is logically equivalent to `p`.
|
forall_prop_domain_congr
theorem forall_prop_domain_congr :
∀ {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop} (h₁ : p₁ = p₂),
(∀ (a : p₂), q₁ ⋯ = q₂ a) → (∀ (a : p₁), q₁ a) = ∀ (a : p₂), q₂ a
This theorem states that for any two propositions `p₁` and `p₂`, and for any two predicate functions `q₁` and `q₂` that map from these propositions to another proposition, if `p₁` equals `p₂` and for all `a` from `p₂`, `q₁` equals `q₂ a`, then the proposition that "for all `a` from `p₁`, `q₁ a` holds" equals the proposition that "for all `a` from `p₂`, `q₂ a` holds". This theorem essentially asserts the congruence of universal quantifications over equal domains of propositions.
More concisely: If `p₁` equals `p₂` and for all `a` in `p₂`, `q₁ a` equals `q₂ a`, then ∀`a` in `p₁, q₁ a` is equal to ∀`a` in `p₂, q₂ a`.
|
eq_true
theorem eq_true : ∀ {p : Prop}, p → p = True
This theorem states that for any proposition `p`, if `p` holds (or is true), then `p` is equal to `True`. In other words, it is asserting that if a certain condition or proposition `p` is satisfied, then we can identify `p` as being `True`. This is a foundational concept in propositional logic used in Lean 4 theorem prover.
More concisely: For any proposition `p` in Lean 4, `p` is equivalent to `True` when `p` holds true.
|
eq_false
theorem eq_false : ∀ {p : Prop}, ¬p → p = False
This theorem states that for any proposition `p`, if `p` is not true (denoted by `¬p`), then `p` is equivalent to `false`. In other words, if we can show that a certain proposition cannot be true, then we can say that this proposition is effectively the same as `false` in our logic system.
More concisely: The negation of a proposition is equivalent to false. ( ∥ ¬p ≡ false ∥)
|
Or.imp_left
theorem Or.imp_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` implies `b`, then the disjunction of `a` and `c` implies the disjunction of `b` and `c`. In other words, if we know that `a` leads to `b`, and we have either `a` or `c` is true, then we can conclude that either `b` or `c` is true.
More concisely: If `a` implies `b`, then `a || c` implies `b || c` (disjunction of `a` and `c` implies disjunction of `b` and `c`).
|
Bool.not_true
theorem Bool.not_true : (!true) = false
This theorem states that the logical negation of true, denoted as '!true' in Lean 4, is equal to false. In other words, if we negate or reverse the boolean value 'true', we obtain 'false'.
More concisely: The logical negation of true is equal to false. (or) !true = false in Lean 4.
|
Bool.and_self
theorem Bool.and_self : ∀ (b : Bool), (b && b) = b
This theorem states that for any boolean value `b`, the logical AND of `b` with itself is always equal to `b`. In other words, if you take a boolean value and AND it with itself, you get the same boolean value back. This is a fundamental property of boolean logic.
More concisely: For any boolean value `b`, `b` and `b` are equal.
|
Bool.not_eq_false
theorem Bool.not_eq_false : ∀ (b : Bool), (¬b = false) = (b = true)
This theorem states that for any boolean value `b`, the statement "not `b` equals false" is equivalent to the statement "`b` equals true". In other words, if the negation of a boolean value is false, then the original boolean value must have been true, and vice versa.
More concisely: The negation of a boolean value is logically equivalent to its complement. That is, `not b` is equivalent to `b = false b = true`.
|
Bool.false_or
theorem Bool.false_or : ∀ (b : Bool), (false || b) = b
This theorem states that for all Boolean values `b`, the result of a logical OR operation between `false` and `b` is `b`. This corresponds to the logical principle that `false` is the identity for the logical OR operation, which means that if any value is logically OR'ed with `false`, it will not change the value.
More concisely: For all Boolean values `b`, `false∨b` equals `b`.
|
and_congr_left_iff
theorem and_congr_left_iff : ∀ {a c b : Prop}, (a ∧ c ↔ b ∧ c) ↔ c → (a ↔ b)
This theorem, `and_congr_left_iff`, states that for any three propositions `a`, `b`, and `c`, the equivalence between "a and c" and "b and c" is equivalent to the implication from `c` to the equivalence of `a` and `b`. In other words, if `c` is true, then "a and c" is equivalent to "b and c" if and only if `a` is equivalent to `b`.
More concisely: For propositions `a`, `b`, and `c`, `(a ∧ c) ≈ (b ∧ c)` if and only if `a ≈ b`.
|
of_eq_true
theorem of_eq_true : ∀ {p : Prop}, p = True → p
This theorem states that for any proposition `p`, if `p` equals `True`, then `p` is true. In other words, it asserts that if we can equate a proposition to the boolean value `True`, then that proposition itself must be true. This theorem is fundamental to the logical foundation, bridging the gap between propositional logic and boolean algebra.
More concisely: If a proposition `p` is equal to `True`, then `p` is true.
|
eq_false'
theorem eq_false' : ∀ {p : Prop}, (p → False) → p = False
This theorem states that for any proposition 'p', if 'p' implies falsehood (denoted as `p → False`), then 'p' is equivalent to false (denoted as `p = False`). Essentially, it suggests that if assuming 'p' leads to a contradiction or a false statement, then 'p' itself must be false. This theorem is a formal statement of the principle of reductio ad absurdum in propositional logic.
More concisely: If `p → False`, then `p = False`. (This theorem formalizes the principle of proof by contradiction or reductio ad absurdum in propositional logic.)
|
forall_congr
theorem forall_congr : ∀ {α : Sort u} {p q : α → Prop}, (∀ (a : α), p a = q a) → (∀ (a : α), p a) = ∀ (a : α), q a := by
sorry
This theorem establishes the congruence of two universally quantified predicates over any sort `α`. Specifically, given two predicates `p` and `q` that map elements of `α` to propositions, if for every element of `α`, `p` and `q` are equal (i.e., they produce the same proposition), then the universal quantification of `p` is equal to the universal quantification of `q`. In other words, if two predicates are equivalent for every element in a set, then their universal quantifications are also equivalent.
More concisely: If two predicates mapping elements of a set to propositions are equal for all elements, then their universal quantifications are equal.
|
and_false
theorem and_false : ∀ (p : Prop), (p ∧ False) = False
This theorem states that for any proposition `p`, the logical conjunction of `p` and `False` is equivalent to `False`. In terms of logical operations, this means that `False` combined with any other statement using an "and" operation results in `False`, regardless of the truth value of the other statement.
More concisely: For all propositions p, p AND False equals False.
|
Bool.or_self
theorem Bool.or_self : ∀ (b : Bool), (b || b) = b
This theorem, `Bool.or_self`, states that for any Boolean value `b`, the logical OR of `b` with itself is equal to `b`. In other words, it's expressing the idempotent property of the logical OR operation in Boolean algebra: "or-ing" a value with itself does not change the value. This is true for both `b = true` and `b = false`.
More concisely: For all Boolean values `b`, `b ∨ b` equals `b`.
|
of_eq_false
theorem of_eq_false : ∀ {p : Prop}, p = False → ¬p
This theorem states that for any proposition `p`, if `p` is equal to `False`, then `p` is not true. In other words, if we have established that a certain proposition is equivalent to `False`, then we can logically conclude that this proposition is not true. This theorem is essentially a formalization of a basic principle in classical logic.
More concisely: If a proposition is equal to False, then it is not true.
|
or_iff_right_of_imp
theorem or_iff_right_of_imp : ∀ {a b : Prop}, (a → b) → (a ∨ b ↔ b)
This theorem states that for any two propositions `a` and `b`, if `a` implies `b` (denoted as `a → b`), then the statement "either `a` or `b` is true" is logically equivalent to the statement "`b` is true". In mathematical terms, this theorem asserts that whenever `a` implies `b`, the logical disjunction `a ∨ b` is equivalent to `b`.
More concisely: If `a` implies `b`, then `a ∨ b` is logically equivalent to `b` in Lean 4 logic.
|
true_or
theorem true_or : ∀ (p : Prop), (True ∨ p) = True
This theorem states that for any proposition `p`, the disjunction of `True` and `p` is always `True`. In other words, no matter what `p` is, `True` OR `p` will always be `True`. In terms of symbolic logic, if you have "True OR anything", it's always guaranteed to be `True`.
More concisely: For all propositions p, True \|\ p holds true. (In the context of Lean 4 logic, where \|\ represents disjunction.)
|
Bool.and_true
theorem Bool.and_true : ∀ (b : Bool), (b && true) = b
This theorem states that for any boolean value `b`, the logical AND of `b` and `true` is equal to `b`. In other words, when a boolean is logically ANDed with `true`, the result is the original boolean itself, regardless of whether it is `true` or `false`. This statement mirrors the principle of identity in Boolean algebra.
More concisely: For any boolean value `b`, `b` and `true` have equal logical AND values. In Lean notation: `(b : bool) => b && true = b`.
|
bne_self_eq_false
theorem bne_self_eq_false : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α), (a != a) = false
This theorem, `bne_self_eq_false`, states that for all types `α` equipped with a binary equality (`BEq`) operation that satisfies the laws of a `LawfulBEq`, the binary non-equality (`!=`) of any element `a` from `α` with itself is always `false`. In more plain terms, it means that an element is never not equal to itself, across all types that permit lawful binary equality operations.
More concisely: For all types `α` with a lawful binary equality operation `BEq`, `a BEq a` holds for all `a : α`. Therefore, `a != a` is false for all `a : α`.
|
Bool.not_eq_true'
theorem Bool.not_eq_true' : ∀ (b : Bool), ((!b) = true) = (b = false)
This theorem states that for any boolean value `b`, the negation of `b` being true is equivalent to `b` being false. In other words, if not `b` equals true, then `b` must be false and vice versa. This is a basic property of boolean logic.
More concisely: The negation of a boolean value is logically equivalent to its negation. In other words, `not b` is equivalent to `b -> false`.
|
Eq.mpr_not
theorem Eq.mpr_not : ∀ {p q : Prop}, p = q → ¬q → ¬p
This theorem states that for any two propositions `p` and `q`, if `p` is equal to `q` and `q` is not true (denoted by `¬q`), then `p` is also not true (denoted by `¬p`). In other words, it provides a means to propagate the falsity of a proposition to another equal proposition.
More concisely: If `p` equals `q` and `q` is false, then `p` is false.
|
not_true_eq_false
theorem not_true_eq_false : (¬True) = False
This theorem states that the negation of the proposition `True` is equal to `False`. In other words, it's saying that if we claim `True` is not true, this is the same as saying `False`. This matches the intuitive understanding of truth values: denying something that is undeniably true gives us falsehood.
More concisely: The negation of `True` is equal to `False`. In mathematical notation: `~(true : Prop) = false`.
|
Bool.and_eq_true
theorem Bool.and_eq_true : ∀ (a b : Bool), ((a && b) = true) = (a = true ∧ b = true)
This theorem states that for any two boolean values `a` and `b`, the boolean 'and' operation (`a && b`) equals `true` if and only if both `a` and `b` are `true`. This reflects the basic logic concept that an 'and' operation only yields `true` when both operands are `true`.
More concisely: For all boolean values `a` and `b`, `a && b` equals `true` if and only if both `a` and `b` are `true`.
|
or_false
theorem or_false : ∀ (p : Prop), (p ∨ False) = p
This theorem is named `or_false` and it states that for all propositions `p`, the logical disjunction of `p` and `False` is simply `p`. In other words, if we take a statement `p` and form a new statement that is the 'or' of `p` and `False`, then the new statement is logically equivalent to just `p`. This makes sense because 'or' is true if either of the components is true, hence 'or' with `False`, which is never true, isn't changing the original proposition.
More concisely: For all propositions p, pOrFalse ≡ p in Lean logic. (Here, pOrFalse represents the logical disjunction of p and False.)
|
ite_cond_eq_true
theorem ite_cond_eq_true : ∀ {α : Sort u} {c : Prop} {x : Decidable c} (a b : α), c = True → (if c then a else b) = a
This theorem states that for any type `α`, proposition `c`, and decidable instance `x` of `c`, along with two variables `a` and `b` of type `α`, if `c` is equivalent to `True`, then the `if` expression evaluates to `a`. In other words, when a condition of an if-then-else expression is true, the expression evaluates to the value in the 'then' branch.
More concisely: For any type `α`, decidable proposition `c`, and values `a`, `b` of type `α`, if `c` is true and `x` is an instance of `decidable c`, then `if c then a else b` equals `a`.
|
dite_cond_eq_false
theorem dite_cond_eq_false :
∀ {α : Sort u} {c : Prop} {x : Decidable c} {t : c → α} {e : ¬c → α} (h : c = False), dite c t e = e ⋯
This theorem, named "dite_cond_eq_false", states that for any type `α` and any proposition `c`, given a decidable instance of `c`, two functions `t` and `e` of types `c → α` and `¬c → α` respectively, if `c` is proven to be `False`, then the expression `dite c t e` (which stands for "if `c` then `t` else `e`") is equal to `e`. In other words, it says that if the condition of a conditional expression is false, the whole expression evaluates to the "else" part.
More concisely: If `c` is a decidable proposition and `t : α → α` and `e : α` are functions, then `dite c t e = e` when `c` is false.
|
Bool.false_and
theorem Bool.false_and : ∀ (b : Bool), (false && b) = false
This theorem states that for any boolean value `b`, the logical "and" operation between `false` and `b` always results in `false`. This is based on standard logical behavior where if one of the operands of an "and" operation is `false`, the entire expression evaluates to `false` regardless of the other operand's value.
More concisely: For all boolean values `b`, `false and b` equals `false`.
|
Bool.and_assoc
theorem Bool.and_assoc : ∀ (a b c : Bool), (a && b && c) = (a && (b && c))
This theorem states that the logical AND operation (denoted by `&&`) is associative for boolean values. That is, for any three boolean values `a`, `b`, and `c`, the result of `a AND b` ANDed with `c` is the same as the result of `a` ANDed with the result of `b AND c`. In mathematical terms, this can be written as `(a ∧ b) ∧ c = a ∧ (b ∧ c)` where `∧` denotes the logical AND operation.
More concisely: The logical AND operation is associative for boolean values, that is, `(a && b) && c = a && (b && c)` for all boolean values `a`, `b`, and `c`.
|
not_false_eq_true
theorem not_false_eq_true : (¬False) = True
This theorem states that the negation of `False` is equal to `True`. In other words, if something is not `False`, then it is `True`. This is a fundamental principle of Boolean logic.
More concisely: The negation of `False` is `True`. Alternatively, `~False = True`.
|
or_iff_left_iff_imp
theorem or_iff_left_iff_imp : ∀ {a b : Prop}, (a ∨ b ↔ a) ↔ b → a
This theorem states that for any two propositions `a` and `b`, the claim that "`a` or `b` is equivalent to `a`" is logically equivalent to the statement "`b` implies `a`". In other words, having the equivalence between "`a` or `b`" and "`a`" is the same as saying if `b` is true, then `a` is also true. This encapsulates a fundamental logical principle used in proofs and argumentation.
More concisely: The theorem asserts that `(a ∨ b) ↔ (b → a)` for any propositions `a` and `b`.
|
Bool.or_eq_true
theorem Bool.or_eq_true : ∀ (a b : Bool), ((a || b) = true) = (a = true ∨ b = true)
This theorem, `Bool.or_eq_true`, states that for all Boolean values `a` and `b`, the condition where the logical OR of `a` and `b` equals `true` is equivalent to the condition where either `a` is `true` or `b` is `true`. In other words, `a OR b` being `true` is the same as either `a` being `true` or `b` being `true` in Boolean logic.
More concisely: For all Boolean values `a` and `b`, `a ∨ b` is equivalent to `a = true ∨ b = true`.
|
and_self
theorem and_self : ∀ (p : Prop), (p ∧ p) = p
This theorem, `and_self`, states that for any proposition `p`, `p` and `p` is equivalent to `p`. In other words, if we claim that two identical propositions are both true (i.e., `p ∧ p`) that is the same as just stating the one proposition `p` itself is true. This theorem applies to any proposition, regardless of its content.
More concisely: For all propositions p, p and p are logically equivalent.
|
Or.imp
theorem Or.imp : ∀ {a c b d : Prop}, (a → c) → (b → d) → a ∨ b → c ∨ d
This theorem states that, given four propositions `a`, `b`, `c`, and `d`, if `a` implies `c` and `b` implies `d`, then `a` OR `b` necessarily implies `c` OR `d`. The implications act as transformation rules: if `a` is true, it would lead to `c` being true, and if `b` is true, it would lead to `d` being true. Hence, if either `a` or `b` is true, then either `c` or `d` must be true as well.
More concisely: If `a` implies `c` and `b` implies `d`, then `a` or `b` implies `c` or `d`.
|
false_or
theorem false_or : ∀ (p : Prop), (False ∨ p) = p
This theorem states that for any proposition `p`, the disjunction of `False` and `p` is equivalent to `p` itself. In other words, it asserts that "False or `p`" is the same as just saying "`p`". This makes sense because in logic, an "or" statement is true if either or both of its components are true, and "False" is by definition not true, so "`False` or `p`" can only be true if `p` is true.
More concisely: For all propositions p, `False`Or p equivalents p.
|
Bool.or_true
theorem Bool.or_true : ∀ (b : Bool), (b || true) = true
This theorem states that for any boolean value 'b', the result of a logical 'or' operation between 'b' and 'true' will always be 'true'. This is because in Boolean logic, 'or' operation with 'true' always results in 'true', regardless of the other operand.
More concisely: For all boolean values 'b', b orb true = true.
|
Bool.or_assoc
theorem Bool.or_assoc : ∀ (a b c : Bool), (a || b || c) = (a || (b || c))
This theorem states that for all boolean variables `a`, `b`, and `c`, the operation of logical disjunction (`||`) is associative. In other words, the order in which the disjunctions are performed does not change the result. If we denote logical disjunction with the symbol $\vee$, this can be written in mathematical notation as $(a \vee b) \vee c = a \vee (b \vee c)$.
More concisely: The logical disjunction operation is associative, that is, for all boolean variables `a`, `b`, and `c`, `(a || b) || c = a || (b || c)`.
|