ne_of_eq_of_ne
theorem ne_of_eq_of_ne : ∀ {α : Sort u_1} {a b c : α}, a = b → b ≠ c → a ≠ c
This theorem, `ne_of_eq_of_ne`, states that for any type `α`, and any three elements `a`, `b`, and `c` of type `α`, if `a` is equal to `b` and `b` is not equal to `c`, then `a` is also not equal to `c`. In other words, transitivity of equality and inequality is preserved.
More concisely: If `a = b` and `b ≠ c`, then `a ≠ c`.
|
apply_ite₂
theorem apply_ite₂ :
∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (f : α → β → γ) (P : Prop) [inst : Decidable P] (a b : α) (c d : β),
f (if P then a else b) (if P then c else d) = if P then f a c else f b d
This theorem states that for any two-argument function `f` and a propositional statement `P`, and given any elements `a`, `b` of type `α` and `c`, `d` of type `β`, applying `f` to the results of two if-then-else statements based on `P` is equivalent to an if-then-else statement based on `P` where the branches are `f` applied to the pairs `(a, c)` and `(b, d)`. In other words, we can move an if-then-else statement outside of a function application without changing the result.
More concisely: For any two-argument function `f` and propositional statement `P`, and elements `a:α`, `b:α`, `c:β`, `d:β`, if `P` then `f (if h:P then a else b) (if h then c else d) = if h then f (a, c) else f (b, d)`, where `if h:Prop then a else b` and `if h:Prop then c else d` are dependent pairs.
|
Iff.not_left
theorem Iff.not_left : ∀ {a b : Prop}, (a ↔ ¬b) → (¬a ↔ b)
This theorem states that for any two propositions `a` and `b`, if `a` is logically equivalent to `not b` (denoted in Lean 4 as `¬b`), then `not a` is logically equivalent to `b`. In other words, if `a` being true means `b` is false, and `a` being false means `b` is true, then the converse also holds: `a` being false means `b` is true, and `a` being true means `b` is false.
More concisely: If `a` is logically equivalent to `not b` in Lean 4, then `not a` is logically equivalent to `b`.
|
ULift.down_injective
theorem ULift.down_injective : ∀ {α : Type u_2}, Function.Injective ULift.down
This theorem states that for all types `α`, the function `ULift.down` is injective. In other words, if `ULift.down` applied to two values gives the same result, then the two original values must have been the same. This means that `ULift.down` preserves distinctness: no two different values will map to the same value. In mathematical terms, if `ULift.down(x) = ULift.down(y)`, then `x = y`. This property is crucial for many mathematical constructions and proofs.
More concisely: For all types `α`, the function `ULift.down` is a bijective function from the universe of `α` to its image under `ULift.down`.
|
not_imp_not
theorem not_imp_not : ∀ {a b : Prop}, ¬a → ¬b ↔ b → a
This theorem states that for any two propositions 'a' and 'b', the statement "not 'a' implies not 'b'" is equivalent to "if 'b' then 'a'". In other words, if the truth of 'b' implies the truth of 'a', then the negation of 'a' must imply the negation of 'b' and vice versa. This is a fundamental theorem in propositional logic that shows the relationship between implications and their negations.
More concisely: The negations of propositions 'a' and 'b' are logically equivalent if and only if 'b' implies 'a' implies 'b' and 'a' implies 'b' implies 'a'.
|
eq_or_ne
theorem eq_or_ne : ∀ {α : Sort u_1} (x y : α), x = y ∨ x ≠ y
This theorem, `eq_or_ne`, states that for any given type `α` (which could be any sort of data, such as a number or a list), and for any two instances `x` and `y` of that type, it is always the case that either `x` equals `y`, or `x` does not equal `y`. This is a fundamental law in logic and mathematics, often referred to as the Law of Excluded Middle.
More concisely: For all types `α` and elements `x, y` of type `α`, we have `x = y < burning_issues_or_x_neq_y >`. Here, `` is the logical OR of `x = y` and `x ≠ y`.
|
em'
theorem em' : ∀ (p : Prop), ¬p ∨ p
This theorem, `em'`, is a statement of the law of excluded middle in propositional logic. It asserts that for any proposition `p`, either `p` is true or `p` is not true, represented as `¬p ∨ p` in Lean 4. In other words, it affirms that every proposition is either true or false, with no third option available.
More concisely: For all propositions p in propositional logic, p or not p holds.
|
pi_congr
theorem pi_congr :
∀ {α : Sort u_1} {β β' : α → Sort u_2}, (∀ (a : α), β a = β' a) → ((a : α) → β a) = ((a : α) → β' a)
This theorem, "pi_congr", states that for any sort `α` and for any two sorts `β` and `β'` that depend on `α`, if for every element `a` of `α` the dependent sort `β a` is equal to `β' a`, then the type of functions from `α` to `β a` is equal to the type of functions from `α` to `β' a`. In other words, if two dependent types are equal for every value in their common domain, then the spaces of functions from the domain to each of the dependent types are also equal.
More concisely: If for all elements `a` of sort `α`, the dependent types `β a` and `β' a` are equal, then the types of functions from `α` to `β a` and functions from `α` to `β' a` are equal.
|
Exists.fst
theorem Exists.fst : ∀ {b : Prop} {p : b → Prop}, Exists p → b
This theorem, `Exists.fst`, states that for any given proposition `b` and a predicate `p` that maps from `b` to a proposition, if there exists an element that satisfies the predicate `p`, then the proposition `b` holds true. In other words, if there is some element in `b` for which the predicate `p` is true, then `b` itself is true.
More concisely: If there exists an element x in type B such that predicate p(x) holds, then proposition B is true.
|
Iff.imp
theorem Iff.imp : ∀ {a b c d : Prop}, (a ↔ c) → (b ↔ d) → (a → b ↔ c → d)
This theorem, known as `Iff.imp`, states that for any four propositions `a`, `b`, `c`, and `d`, if `a` is logically equivalent to `c` and `b` is logically equivalent to `d`, then the implication `a → b` is logically equivalent to the implication `c → d`. In other words, if two pairs of propositions are equivalent to each other, the implications between the propositions of each pair are also equivalent.
More concisely: If `a` is logically equivalent to `c` and `b` is logically equivalent to `d`, then `(a → b)` is logically equivalent to `(c → d)`.
|
Membership.mem.ne_of_not_mem
theorem Membership.mem.ne_of_not_mem :
∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {s : β} {a b : α}, a ∈ s → b ∉ s → a ≠ b
The theorem `Membership.mem.ne_of_not_mem` states that for any two elements `a` and `b` of some type `α`, and any set `s` of type `β`, if `a` is a member of `s` and `b` is not a member of `s`, then `a` and `b` must not be equal. This theorem is an alias of `ne_of_mem_of_not_mem` and applies in any context where a `Membership` relation is defined between `α` and `β`.
More concisely: If `a` is in `s` and `b` is not in `s`, then `a` and `b` are distinct.
|
or_not_of_imp
theorem or_not_of_imp : ∀ {a b : Prop}, (a → b) → b ∨ ¬a
This theorem, `or_not_of_imp`, states that for any two propositions `a` and `b`, if `a` implies `b`, then either `b` is true or `a` is not true. In the language of logic, this is a demonstration of the principle of the excluded middle in the context of implications. This means that if we have an implication from `a` to `b`, there are no other possibilities outside of `b` being true or `a` being false.
More concisely: If `a` implies `b`, then `b` or not-`a`.
|
Mathlib.Logic.Basic._auxLemma.32
theorem Mathlib.Logic.Basic._auxLemma.32 : ∀ {α : Sort u_1} (y : α) (p : α → Prop), (∃ x, x = y ∨ p x) = True := by
sorry
This theorem states that for any two types `α` and `β`, and functions `f : α → β`, `p : α → Prop`, and `q : β → Prop`, there is an equivalence between two existential statements: (1) there exists an element `b` of type `β` such that there exists an element `a` of type `α` where `p a` and `f a = b` hold, and `q b` also holds; and (2) there exists an element `a` of type `α` such that `p a` and `q (f a)` hold. Essentially, it demonstrates how quantifiers and conditions can be rearranged without changing the underlying logical proposition.
More concisely: For any functions `f : α → β`, `p : α → Prop`, and `q : β → Prop`, the statements "exists `a : α` such that `p a` and `f a = b` for some `b : β` with `q b`" and "exists `a : α` such that `p a` and `q (f a)`" are logically equivalent.
|
Eq.trans_ne
theorem Eq.trans_ne : ∀ {α : Sort u_1} {a b c : α}, a = b → b ≠ c → a ≠ c
This theorem, named `Eq.trans_ne`, states that for any type `α` and any three elements `a`, `b`, and `c` of that type, if `a` is equal to `b` and `b` is not equal to `c`, then `a` is not equal to `c`. In other words, it provides a transitive property for inequality, using an intermediary equality.
More concisely: If `a = b` and `b ≠ c`, then `a ≠ c`.
|
em
theorem em : ∀ (p : Prop), p ∨ ¬p
This theorem, also known as Diaconescu's theorem, states that for any proposition 'p', either 'p' is true or 'p' is not true. This is an instance of the principle of the excluded middle, derived from the axiom of choice, function extensionality, and propositional extensionality. In mathematical notation, for any proposition `p`, the result is `p ∨ ¬p`, meaning 'p' or not 'p'.
More concisely: For any proposition `p`, the negation of `p` exists and is equivalent to `p`'s negation, thus `p ∨ ¬p` holds. (This statement represents the principle of excluded middle derived from given axioms in Lean 4.)
|
not_and_or
theorem not_and_or : ∀ {a b : Prop}, ¬(a ∧ b) ↔ ¬a ∨ ¬b
This theorem is one of De Morgan's laws, stating that the negation of a conjunction between two propositions is logically equivalent to the disjunction of the negations of those two propositions. In other words, for any two properties 'a' and 'b', the proposition "not (a and b)" is equivalent to the proposition "not a or not b".
More concisely: The negation of the conjunction of propositions a and b is logically equivalent to the disjunction of their negations.
|
not_imp
theorem not_imp : ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b
This theorem states that for any two propositions `a` and `b`, the negation of the implication from `a` to `b` is equivalent to the conjunction of `a` and the negation of `b`. In other words, denying that `a` implies `b` is the same as asserting that `a` is true and `b` is false.
More concisely: ⊥ ∘ (a → b) ≡ a ∧ ⌐b, where ⊥ is the logical falsity, a and b are propositions, and ∘ represents logical composition (implication). This statement asserts that the logical negation of an implication is equivalent to the conjunction of the premise and the negation of the conclusion.
|
and_forall_ne
theorem and_forall_ne : ∀ {α : Sort u_1} {p : α → Prop} (a : α), (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b := by
sorry
This theorem states that for any type `α` and any property `p` of `α`, given an element `a` of `α`, the property `p` holds for `a` and for all other elements `b` of `α` that are not equal to `a` if and only if the property `p` holds for all elements `b` of `α`. In other words, if you know that a property is true for one specific element and all other different elements, then it is indeed true for all elements of the type.
More concisely: For any type `α` and property `p` of `α`, if `p` holds for all `a` in `α` and all other distinct `b` in `α`, then `p` holds for all elements in `α`.
|
congr_heq
theorem congr_heq :
∀ {α β : Sort u_2} {γ : Sort u_3} {f : α → γ} {g : β → γ} {x : α} {y : β}, HEq f g → HEq x y → f x = g y
This theorem, named `congr_heq`, asserts that for any types `α` and `β` of the same universe `u_1`, along with another type `γ` in a potentially different universe `u_2`, as well as functions `f: α → γ` and `g: β → γ`, and elements `x: α` and `y: β`, if `f` and `g` are heterogeneously equal (i.e., `HEq f g`) and `x` and `y` are also heterogeneously equal (`HEq x y`), then the results of applying `f` and `g` to `x` and `y` respectively are equal (i.e., `f x = g y`). Essentially, it shows that if two functions are the same, and two elements are the same (even if of different types), applying the same function to those elements yields the same result.
More concisely: Given functions `f: α → γ` and `g: β → γ` between types `α`, `β`, and `γ` in possibly different universes, and elements `x: α` and `y: β` such that `HEq f g` and `HEq x y`, then `f x = g y`.
|
Xor'.or
theorem Xor'.or : ∀ {a b : Prop}, Xor' a b → a ∨ b
This theorem states that for any two propositions 'a' and 'b', if the exclusive or 'Xor'' of 'a' and 'b' is true, then the inclusive or (denoted as 'a ∨ b' in Lean and similarly in LaTeX) of 'a' and 'b' must also be true. In other words, if 'a' and 'b' cannot both be true or false (the definition of 'Xor''), then at least one of 'a' or 'b' is true.
More concisely: If $a \mathop{\mathsf{Xor}} b$ holds, then $a \vee b$ is true.
|
not_forall_not
theorem not_forall_not : ∀ {α : Sort u_1} {p : α → Prop}, (¬∀ (x : α), ¬p x) ↔ ∃ x, p x
This theorem, `not_forall_not`, states that for any type `α` and for any property `p` of `α`, the negation of the statement "For all `x` of type `α`, `p` does not hold" is logically equivalent to the existence statement "There exists an `x` of type `α` such that `p` holds". In other words, if it is not the case that `p` fails for all `x`, then there exists some `x` for which `p` is true.
More concisely: The negation of "for all x in α, not p(x)" is logically equivalent to "there exists x in α such that p(x) holds".
|
Mathlib.Logic.Basic._auxLemma.23
theorem Mathlib.Logic.Basic._auxLemma.23 : ∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], (α → b) = b
This theorem states that for any type `α` that is a subsingleton (i.e., a type with at most one distinct element), and any property `p` that elements of `α` can have, the existence of a unique element `x` such that `p x` holds is equivalent to the existence of an element `x` such that `p x` holds. In other words, if `α` is a subsingleton, then uniqueness is redundant because there is either zero or one element in `α` satisfying `p`, and therefore the existence of a unique `x` satisfying `p` is the same as the existence of `x` satisfying `p`.
More concisely: If `α` is a subsingleton type, then the unique existence and existence statements for a property `p` are equivalent.
|
Fact.out
theorem Fact.out : ∀ {p : Prop} [self : Fact p], p
The theorem `Fact.out` states that for any propositional statement `p`, if there is an instance of the `Fact p` typeclass, then `p` must be true. In other words, if a proof exists for `p` (represented by the `Fact p` instance), then `p` is a valid proposition. The function `Fact.out` unwraps and retrieves the proof (or witness) for `p` from the `Fact p` instance.
More concisely: If a type-level proposition `p` has a proof instance of type `Fact p`, then `p` is a true proposition.
|
iff_not_comm
theorem iff_not_comm : ∀ {a b : Prop}, (a ↔ ¬b) ↔ (b ↔ ¬a)
This theorem states that for any two propositions `a` and `b`, the statement "if and only if `a` then not `b`" is equivalent to the statement "if and only if `b` then not `a`". In other words, it is asserting that the logical relationship between `a` and `b` is symmetric, such that if `a` implies that `b` is not true, then `b` must also imply that `a` is not true, and vice versa.
More concisely: The theorem asserts that for all propositions `a` and `b`, the logical equivalence `(a ↔ ¬ b) ↔ (b ↔ ¬ a)` holds.
|
iff_eq_eq
theorem iff_eq_eq : ∀ {a b : Prop}, (a ↔ b) = (a = b)
This theorem, named `iff_eq_eq`, states that for all propositions `a` and `b`, the logical equivalence of `a` and `b` (denoted as `a ↔ b` in Lean 4) is equal to the statement that `a` and `b` are the same proposition (denoted as `a = b` in Lean 4). In other words, it asserts the equivalence between logical equivalence and propositional equality in the context of propositional logic.
More concisely: The logical equivalence of propositions `a` and `b` (`a ↔ b`) is equivalent to their propositional equality (`a = b`) in propositional logic.
|
by_contra
theorem by_contra : ∀ {p : Prop}, (¬p → False) → p
The theorem `by_contra` is an alias of `by_contradiction`. It states that for any proposition `p`, if assuming `¬p` (not `p`) leads to a contradiction (i.e., something that is always false), then `p` must be true. This is a primary form of proof in classical logic known as proof by contradiction.
More concisely: If assuming the negation of a proposition leads to a contradiction, then the proposition is true.
|
Mathlib.Logic.Basic._auxLemma.2
theorem Mathlib.Logic.Basic._auxLemma.2 : ∀ {a : Prop}, (a → False) = ¬a
The theorem `Mathlib.Logic.Basic._auxLemma.2` states that, for any proposition `a`, the proposition `a → False` is equivalent to `¬a`. In natural language, it says that asserting "if `a` then false" is the same as saying "`a` is not true" or "not `a`". This sets up a logical equivalence between implication towards falsehood and negation, which are fundamental constructs in propositional logic.
More concisely: The theorem `Mathlib.Logic.Basic._auxLemma.2` asserts that for any proposition `a`, the implications `a → False` and `¬a` are logically equivalent.
|
dite_apply
theorem dite_apply :
∀ {α : Sort u_1} {σ : α → Sort u_2} (P : Prop) [inst : Decidable P] (f : P → (a : α) → σ a) (g : ¬P → (a : α) → σ a)
(a : α), dite P f g a = if h : P then f h a else g h a
This theorem states that for any property `P`, which is decidable, and two functions `f` and `g` defined on the elements of type `α` for when `P` holds and when `P` does not hold respectively, the application of the dependent `if-then-else` function (`dite`) to an element `a` of type `α` will yield the same result as applying `f` to `a` if `P` holds, and `g` to `a` otherwise. It essentially describes how `dite`, which constructs a dependent function over a type `α` based on a decidable proposition `P`, behaves when applied to an element of `α`.
More concisely: For any decidable property `P` and functions `f` and `g` on type `α`, if `a` is an element of `α` such that `P a` holds then `dite P f g a = f a`, and if `P a` does not hold then `dite P f g a = g a`.
|
of_not_not
theorem of_not_not : ∀ {a : Prop}, ¬¬a → a
This theorem, named `of_not_not`, states that for any proposition `a`, if it is not the case that `a` is not true (denoted as ¬¬a), then `a` is indeed true. In other words, this theorem is about the principle of double negation in classical logic, where denying the denial of a proposition implies the truth of the proposition itself.
More concisely: If not (not p), then p holds in classical logic.
|
by_contradiction
theorem by_contradiction : ∀ {p : Prop}, (¬p → False) → p
This theorem, referred to as `by_contradiction`, states that for any proposition `p`, if the negation of `p` (expressed as `¬p`) leads to a contradiction (expressed as `→ False`), then `p` must be true. In other words, it captures the principle of proof by contradiction: if assuming the opposite of a proposition results in a contradiction, then the proposition itself must be true.
More concisely: If the negation of a proposition leads to a contradiction, then the proposition is true.
|
ite_apply
theorem ite_apply :
∀ {α : Sort u_1} {σ : α → Sort u_2} (P : Prop) [inst : Decidable P] (f g : (a : α) → σ a) (a : α),
(if P then f else g) a = if P then f a else g a
This theorem states that for any proposition `P`, decidable instance `inst`, two functions `f` and `g` that output a type `σ` depending on an arbitrary input `a : α`, and a value `a : α`, applying an `if-then-else` statement to a value is equivalent to applying the value to the function determined by the `if-then-else` statement. In other words, whether the `if-then-else` statement is applied before or after the function doesn't change the result.
More concisely: For any decidable proposition `P`, function `f : α → σ`, value `a : α`, and boolean `b : Prop`, `(if h : P then f else g) a = if h then f a else g a`.
|
ne_or_eq
theorem ne_or_eq : ∀ {α : Sort u_1} (x y : α), x ≠ y ∨ x = y
This theorem, `ne_or_eq`, states that for any type `α` and any two elements `x` and `y` of that type, `x` and `y` are either not equal (`x ≠ y`) or they are equal (`x = y`). Basically, this theorem represents the law of excluded middle for equality, asserting that either `x` equals `y` or `x` does not equal `y`, with no third option possible.
More concisely: For all types `α` and elements `x, y` of type `α`, `x = y` or `x ≠ y`.
|
ball_or_left
theorem ball_or_left :
∀ {α : Sort u_1} {r p q : α → Prop}, (∀ (x : α), p x ∨ q x → r x) ↔ (∀ (x : α), p x → r x) ∧ ∀ (x : α), q x → r x
This theorem states that for any type `α` and predicates `p`, `q`, and `r` over `α`, the proposition that for all `x` of type `α`, `r x` is true whenever either `p x` or `q x` is true, is equivalent to the conjunction of the two propositions: for all `x` of type `α`, `r x` is true whenever `p x` is true, and for all `x` of type `α`, `r x` is true whenever `q x` is true. So in mathematical terms, this theorem proves that `(∀x, p(x) ∨ q(x) ⇒ r(x)) ↔ (∀x, p(x) ⇒ r(x)) ∧ (∀x, q(x) ⇒ r(x))`.
More concisely: The theorem asserts that for any type `α` and predicates `p`, `q`, and `r` over `α`, the implication `(p(x) ∨ q(x) → r(x))` is logically equivalent to the conjunction `(∀x, p(x) → r(x)) ∧ (∀x, q(x) → r(x))`.
|
dec_em
theorem dec_em : ∀ (p : Prop) [inst : Decidable p], p ∨ ¬p
This theorem, `dec_em`, is an alias for `Decidable.em`. It states that for any proposition `p`, given that `p` is decidable (specified by the typeclass instance `Decidable p`), either `p` is true or `p` is not true. This is a rephrasing of the law of excluded middle in the context of decidable propositions. In mathematical terms, for any proposition `p`, if we can decide whether `p` holds or not, then it is guaranteed that either `p` holds or `p` does not hold, and there are no other possibilities.
More concisely: If a proposition is decidable, then it is either true or false.
|
Iff.not
theorem Iff.not : ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
This theorem, referred to as "Iff.not", asserts that for any two propositions `a` and `b`, if `a` is equivalent to `b` (denoted by `a ↔ b`), then the negation of `a` is equivalent to the negation of `b` (denoted by `¬a ↔ ¬b`). Essentially, it is stating that the equivalence of two propositions remains unchanged when both propositions are negated. This theorem serves as an alias for the `not_congr` theorem in Lean.
More concisely: For all propositions `a` and `b`, if `a ↔ b`, then `¬a ↔ ¬b`.
|
exists_swap
theorem exists_swap : ∀ {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop}, (∃ x y, p x y) ↔ ∃ y x, p x y
This theorem, `exists_swap`, states that for any types `α` and `β` and any property `p` that relates an instance of `α` and `β`, the existence of a pair `(x, y)` such that `p x y` is true is equivalent to the existence of a pair `(y, x)` such that `p x y` is true. In terms of logic, this theorem is stating that the order of quantifiers in an existential statement does not affect the truth of the statement.
More concisely: For any types `α`, `β`, and property `p(x, y)`: the existence of `x` and `y` such that `p x y` holds is equivalent to the existence of `y` and `x` such that `p x y` holds.
|
Mathlib.Logic.Basic._auxLemma.16
theorem Mathlib.Logic.Basic._auxLemma.16 : ∀ (a b : Prop), ((a → b) ∧ (b → a)) = (a ↔ b)
This theorem states that for any type `α`, if you have two elements `a` and `b` of this type, then the statement "a equals b" is logically equivalent to "b equals a". In other words, equality is symmetric in Lean's logic: if `a` is equal to `b`, then `b` is equal to `a`, and vice versa. This is a fundamental principle of equality in mathematics, formalized here in Lean 4's type theory.
More concisely: In Lean 4's type theory, for all types `α` and elements `a` and `b` of type `α`, the equality `a = b` is logically equivalent to `b = a`.
|
exists_true_left
theorem exists_true_left : ∀ (p : True → Prop), (∃ (x : True), p x) ↔ p True.intro
This theorem, `exists_true_left`, states that for any proposition `p` that depends on a value of type `True`, the existence of a `True` value `x` such that `p x` is true is logically equivalent to `p True.intro` being true. Here, `True.intro` is the unique value of type `True`. In other words, if there exists a truth value satisfying the proposition `p`, then the proposition `p` applied to the truth value is true, and vice versa.
More concisely: For any proposition `p` that depends on a value of type `True`, the existence of a `True` value `x` such that `p x` holds is logically equivalent to `p True`.
|
Decidable.eq_or_ne
theorem Decidable.eq_or_ne : ∀ {α : Sort u_1} (x y : α) [inst : Decidable (x = y)], x = y ∨ x ≠ y
This theorem states that for any sort `α` and any two elements `x` and `y` of that sort, where there is a decidable equality between `x` and `y`, it is always the case that `x` is either equal to `y` or `x` is not equal to `y`. Here, the sort `α` can be a type or a type of types, `x` and `y` are particular instances of `α`, and the `Decidable` instance provides a mechanism for deciding whether or not `x = y` is true or false. Essentially, this is an embodiment of the law of excluded middle for decidable propositions.
More concisely: For any decidable type `α` and its elements `x` and `y`, if `x = y` is decidable then `x = y` or `x ≠ y`.
|
ball_congr
theorem ball_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)
This theorem states that given any type `α`, a predicate `p` on `α`, and two predicates `P` and `Q` that are dependent on both `α` and the truth of `p`, if for all `α` for which `p` is true, `P` is equivalent to `Q`, then the statement that `P` is true for all `α` for which `p` is true is equivalent to the statement that `Q` is true for all `α` for which `p` is true. In simpler terms, if two conditions `P` and `Q` are equivalent for all elements satisfying a certain property `p`, then the universal statements "All elements that satisfy `p` also satisfy `P`" and "All elements that satisfy `p` also satisfy `Q`" are also equivalent.
More concisely: If for all `α` with `p(α)`, `P(α)` is equivalent to `Q(α)`, then `∀α. p(α) → P(α)` is equivalent to `∀α. p(α) → Q(α)`.
|
Ne.ite_eq_left_iff
theorem Ne.ite_eq_left_iff :
∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a b : α}, a ≠ b → ((if P then a else b) = a ↔ P)
The theorem states that for any two elements `a` and `b` of a certain type `α`, and a proposition `P` that is decidable (meaning its truth value can be determined), if `a` is not equal to `b`, then the if-then-else statement "if `P` then `a` else `b`" is equal to `a` if and only if `P` is true. This theorem characterizes the conditions under which an if-then-else statement with distinct cases is equal to one of its branches.
More concisely: For any `α`, `a` and `b` in `α`, and decidable proposition `P` over `α`, if `a ≠ b` then `if P then a else b = a <=> P`.
|
Ne.ne_or_ne
theorem Ne.ne_or_ne : ∀ {α : Sort u_1} {x y : α} (z : α), x ≠ y → x ≠ z ∨ y ≠ z
This theorem, `Ne.ne_or_ne`, asserts that for any type `α` and any three elements `x`, `y`, and `z` of `α`, if `x` is not equal to `y`, then either `x` is not equal to `z`, or `y` is not equal to `z`. This is a basic property of inequality in any set or type, and can be used to reason about different elements in a type or set.
More concisely: If `x ≠ y` in type `α`, then `x ≠ z` or `y ≠ z`.
|
ExistsUnique.elim₂
theorem ExistsUnique.elim₂ :
∀ {α : Sort u_3} {p : α → Sort u_4} [inst : ∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop} {b : Prop},
(∃! x, ∃! h, q x h) → (∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b) → b
This theorem states that for any type `α`, any predicate `p` on `α`, and any property `q` depending on `α` and `p α`, if there exists a unique element `x` and `h` such that `q x h` holds, then for all `x` and `h` where `q x h` holds, if for all `y` and `hy` where `q y hy` holds, `y` is equal to `x`, then some property `b` holds. The predicate `p` is assumed to be a subsingleton, which means that there is at most one proof of `p x` for any `x`.
More concisely: If for any type `α`, predicate `p` on `α`, and property `q` such that `p` is a subsingleton, there exists a unique `x` and `h` such that `q x h` holds, and for all `x` and `h` where `q x h` holds, if `x = y` implies `h = hy`, then some property `b` holds for all such `x` and `h`.
|
imp_iff_or_not
theorem imp_iff_or_not : ∀ {b a : Prop}, b → a ↔ a ∨ ¬b
This theorem, `imp_iff_or_not`, states that for any two propositions `a` and `b`, the implication `b → a` (if `b` then `a`) is equivalent to `a ∨ ¬b` (either `a` is true, or `b` is not true). This is a logical equivalence principle in propositional logic.
More concisely: The logical equivalence of `(b → a)` and `(a ∨ ¬b)` holds for all propositions `a` and `b`.
|
forall_true_left
theorem forall_true_left : ∀ (p : True → Prop), (∀ (x : True), p x) ↔ p True.intro
This theorem, `forall_true_left`, states that for any property `p` that depends on a statement being `True`, the property holds for all `True` values if and only if the property holds for `True.intro`. In other words, given any proposition `p` that is a function of a `True` value, saying "for all `True` values, `p` holds" is equivalent to saying "`p` holds for `True.intro`". This is because `True.intro` is the only instance of `True`, so any statement about all `True` values is really just a statement about `True.intro`.
More concisely: For any property `p` that depends on a statement being `True`, `p` holds for all `True` values if and only if `p` holds for `True.intro`.
|
Ne.trans_eq
theorem Ne.trans_eq : ∀ {α : Sort u_1} {a b c : α}, a ≠ b → b = c → a ≠ c
This theorem, named `Ne.trans_eq`, is an alias of `ne_of_ne_of_eq`. It states that for any type `α` and any three elements `a`, `b`, and `c` of that type, if `a` is not equal to `b` and `b` is equal to `c`, then `a` is not equal to `c`. In other words, if `a` is not equal to `b` and `b` turns out to be the same as `c`, `a` cannot be equal to `c`.
More concisely: If `a` is not equal to `b` and `b` equals `c`, then `a` is not equal to `c`.
|
forall_swap
theorem forall_swap :
∀ {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop}, (∀ (x : α) (y : β), p x y) ↔ ∀ (y : β) (x : α), p x y := by
sorry
This theorem, `forall_swap`, states that for any two types `α` and `β` and any property `p` that takes an element of `α` and an element of `β`, the proposition that `p` holds for all `x` of type `α` and `y` of type `β` is logically equivalent to the proposition that `p` holds for all `y` of type `β` and `x` of type `α`. In other words, when defining a property that applies to every pair of elements from two types, the order in which we express the quantifiers does not matter.
More concisely: For any types `α` and `β` and property `p(x : α, y : β)`, the propositions `∀x, ∀y, p x y` and `∀y, ∀x, p x y` are logically equivalent.
|
bex_def
theorem bex_def : ∀ {α : Sort u_1} {p q : α → Prop}, (∃ x, ∃ (_ : p x), q x) ↔ ∃ x, p x ∧ q x
This theorem states that for any type `α` and any two properties `p` and `q` that can apply to elements of this type, the assertion that there exists an element `x` of `α` such that `p(x)` holds and `q(x)` holds is logically equivalent to the assertion that there is an element `x` of `α` for which both `p(x)` and `q(x)` hold simultaneously. In other words, it claims that the nested existence quantifiers can be flattened into one existence quantifier followed by a conjunction of properties.
More concisely: For any type `α` and properties `p` and `q` on `α`, the existence of an element `x` in `α` satisfying both `p(x)` and `q(x)` is logically equivalent to the existence of an element `x` in `α` such that `p(x)` and `q(x)` hold separately.
|
not_iff_not
theorem not_iff_not : ∀ {a b : Prop}, (¬a ↔ ¬b) ↔ (a ↔ b)
This theorem states that for any two propositions 'a' and 'b', the equivalence of the negations of 'a' and 'b' (¬a is equivalent to ¬b) if and only if 'a' is equivalent to 'b'. That is, if 'a' and 'b' are either both true or both false, then their negations are also both true or both false, and conversely, if the negations of 'a' and 'b' are both true or both false, then 'a' and 'b' are also both true or both false.
More concisely: The negations of propositions 'a' and 'b' are equivalent if and only if 'a' and 'b' are logically equivalent.
|
imp_forall_iff
theorem imp_forall_iff : ∀ {α : Type u_3} {p : Prop} {q : α → Prop}, (p → ∀ (x : α), q x) ↔ ∀ (x : α), p → q x := by
sorry
This theorem states that, for any type `α`, a proposition `p`, and a property `q` that depends on `α`, the conditional statement "if `p` then for all `x` of type `α`, `q` holds true for `x`" is logically equivalent to the statement "for all `x` of type `α`, if `p` then `q` holds true for `x`". In other words, it's safe to move a universal quantifier (`∀`) across a conditional (`→`), in either direction. This kind of swapping is generally helpful for simplifying logical expressions in mathematical proofs.
More concisely: For any type `α`, proposition `p`, and property `q` depending on `α`, the conditional "p → ∀x:α. q x" is logically equivalent to "∀x:α. p → q x".
|
Or.rotate
theorem Or.rotate : ∀ {a b c : Prop}, a ∨ b ∨ c → b ∨ c ∨ a
This theorem, referred to as `Or.rotate`, is essentially another form or alias for the forward direction of the `or_rotate` theorem. It takes in three propositions: `a`, `b`, and `c`. If the disjunction `a ∨ b ∨ c` is true, then the theorem guarantees that the disjunction `b ∨ c ∨ a` is also true. In simple terms, it rotates the terms in an OR operation, moving the first term to the end.
More concisely: If `a ∨ b ∨ c` holds, then `b ∨ c ∨ a` also holds. (Disjunction is commutative up to cyclic permutations.)
|
Not.decidable_imp_symm
theorem Not.decidable_imp_symm : ∀ {a b : Prop} [inst : Decidable a], (¬a → b) → ¬b → a
This theorem, `Not.decidable_imp_symm`, is an alias for `Decidable.not_imp_symm`. It states that for any two propositions `a` and `b` where `a` is decidable, if `b` can be derived when `a` is not true (`¬a → b`), and if `b` is not true (`¬b`), then `a` must be true. In other words, it represents the logical principle that if the negation of a proposition implies another proposition, and that other proposition is false, then the original proposition must be true.
More concisely: If `a` is a decidable proposition and `b` implies `¬a` whenever `¬b` holds, then `a` is true.
|
Mathlib.Logic.Basic._auxLemma.40
theorem Mathlib.Logic.Basic._auxLemma.40 : ∀ (p : True → Prop), (∀ (x : True), p x) = p True.intro
This theorem, named `Mathlib.Logic.Basic._auxLemma.40`, states that for any type `α`, any property `p` of type `α`, and any element `a'` of type `α`, the existence of an element `a` such that `p a` holds and that `a'` is equal to `a`, is equivalent to the property `p` holding for `a'`. In other words, there exists some `a` satisfying `p` and equal to `a'` if and only if `a'` satisfies `p`.
More concisely: For any type `α` and property `p` of `α`, an element `a'` satisfies `p` if and only if there exists an `a` equal to `a'` such that `p a` holds.
|
ExistsUnique.intro₂
theorem ExistsUnique.intro₂ :
∀ {α : Sort u_3} {p : α → Sort u_4} [inst : ∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop} (w : α)
(hp : p w), q w hp → (∀ (y : α) (hy : p y), q y hy → y = w) → ∃! x, ∃! hx, q x hx
This theorem states that given a type `α`, a predicate `p` on `α`, a property `q` that holds for an element `x` of `α` and a proof `p x`, and an object `w` of type `α` for which `p w` holds, if `q w p` also holds, and for all other `y` in `α` for which `p y` and `q y p` holds, `y` equals `w`, then there exists a unique `x` with a proof `p x` for which `q x p` holds. In simpler terms, it says that if a property holds uniquely for an element (under a certain predicate), then there exists a unique element for which the property holds. The uniqueness is guaranteed by the `Subsingleton` clause which ensures that there is at most one proof of `p x` for any `x`.
More concisely: Given a type `α`, a predicate `p` on `α`, a property `q` on `α` x `Prop`, and assuming `Subsingleton α`, if for all `x` and `y` in `α` with `p x` and `p y` and `q x p x` and `q y p y` imply `x = y`, then there exists a unique `x` with `p x` and `q x p x`.
|
Iff.iff
theorem Iff.iff : ∀ {p₁ p₂ q₁ q₂ : Prop}, (p₁ ↔ p₂) → (q₁ ↔ q₂) → ((p₁ ↔ q₁) ↔ (p₂ ↔ q₂))
This theorem, named `Iff.iff`, states that for any four propositions `p₁`, `p₂`, `q₁`, and `q₂`, if `p₁` is logically equivalent to `p₂` and `q₁` is logically equivalent to `q₂`, then the logical equivalence of `p₁` to `q₁` is the same as the logical equivalence of `p₂` to `q₂`. In other words, it allows us to substitute equivalent propositions in logical equivalence expressions without changing the truth value of the whole expression.
More concisely: If p₁ ≡ p₂ and q₁ ≡ q₂, then p₁ ≡ q₁. (Logical equivalence is transitive.)
|
not_or_of_imp
theorem not_or_of_imp : ∀ {a b : Prop}, (a → b) → ¬a ∨ b
This theorem states that for any two propositions 'a' and 'b', if 'a' implies 'b' then either 'a' is not true or 'b' is true. In other words, given a logical implication from 'a' to 'b', it follows that either 'a' is false or 'b' is true. This is a standard construct in propositional logic.
More concisely: If `a` implies `b`, then `~a` or `b` is true. (In Lean's logical syntax: `(a → b) <-> (~a V b)`)
|
Iff.or
theorem Iff.or : ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∨ b ↔ c ∨ d)
This theorem, named `Iff.or`, states that for any four propositions `a`, `c`, `b`, and `d`, if `a` is logically equivalent to `c` and `b` is logically equivalent to `d`, then the logical disjunction of `a` and `b` (`a ∨ b`) is logically equivalent to the logical disjunction of `c` and `d` (`c ∨ d`). This is essentially an alias for the `or_congr` theorem.
More concisely: If `a` is equivalent to `c` and `b` is equivalent to `d`, then `a ∨ b` is equivalent to `c ∨ d`.
|
Iff.not_right
theorem Iff.not_right : ∀ {a b : Prop}, (¬a ↔ b) → (a ↔ ¬b)
This theorem, `Iff.not_right`, states that for any two propositions `a` and `b`, if the negation of `a` is logically equivalent to `b`, then `a` is logically equivalent to the negation of `b`. In other words, if `¬a` is the same as `b` (meaning `¬a` implies `b` and `b` implies `¬a`), then `a` must be the same as `¬b` (meaning `a` implies `¬b` and `¬b` implies `a`).
More concisely: If `a` is logically equivalent to the negation of `b`, then `b` is logically equivalent to the negation of `a`.
|
Mathlib.Logic.Basic._auxLemma.33
theorem Mathlib.Logic.Basic._auxLemma.33 : ∀ {α : Sort u_1} (y : α) (p : α → Prop), (∃ x, p x ∨ x = y) = True := by
sorry
This theorem states that for any two types `α` and `β` and a function `f` from `α` to `β` and a property `p` of `β`, there exists an element `b` of `β` which is the image of some `α` under `f` and that satisfies `p`, if and only if there exists an `α` such that `p` holds for its image under `f`. In other words, it connects the existence of an element with a certain property after a function application with the existence of a preimage with this property.
More concisely: For any function `f` between types `α` and `β` and property `p` of `β`, there exists an `α` mapping to `β` under `f` with property `p` if and only if there exists an element `b` in the image of `f` with property `p`.
|
forall₂_imp
theorem forall₂_imp :
∀ {α : 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
This theorem says that for all types `α` and indexed type `β`, and for any predicates `p` and `q` that take two arguments (an element of `α` and an element of `β` indexed by that `α`), if it is true that `p a b` implies `q a b` for all `a` in `α` and `b` in `β a`, and if it is true that `p a b` holds for all `a` and `b`, then it must also be true that `q a b` holds for all `a` and `b`. Essentially, it's stating a kind of transitivity rule for universally quantified, two-argument predicates.
More concisely: If `p(a, b)` implies `q(a, b)` for all `a` and `b`, and `∀a, ∃b, p(a, b)`, then `∀a, ∀b, q(a, b)`.
|
Fact.elim
theorem Fact.elim : ∀ {p : Prop}, Fact p → p
This theorem, named "Fact.elim", asserts that for any proposition `p`, if `p` is a fact, then `p` itself is true. In other words, given an instance of the `Fact` typeclass for a particular proposition `p`, it provides a proof of `p`. The `Fact` typeclass in Lean is a way of asserting that a certain proposition is universally true.
More concisely: For any proposition `p` that is an instance of the `Fact` typeclass in Lean, `p` holds true.
|
not_iff_comm
theorem not_iff_comm : ∀ {a b : Prop}, (¬a ↔ b) ↔ (¬b ↔ a)
This theorem states that for any two propositions `a` and `b`, the statement "not `a` is equivalent to `b`" is itself equivalent to the statement "not `b` is equivalent to `a`". In other words, the logical not operation can be "transferred" across an equivalence (iff) from one side to the other, and this process is commutative.
More concisely: The logical negation of an equivalence is equivalent to the reversed equivalence.
|
apply_dite₂
theorem apply_dite₂ :
∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (f : α → β → γ) (P : Prop) [inst : Decidable P] (a : P → α)
(b : ¬P → α) (c : P → β) (d : ¬P → β),
f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
This theorem states that for any two-argument function `f`, and any proposition `P` with a decidable instance, if `f` is applied to two dependent `if-then-else` constructs (`dite`), the result is equivalent to another `if-then-else` construct where the `f` is applied to each of the branches separately. In other words, the operation of the function `f` over `dite` structures is distributive: `f` can be distributed over the true and false branches of the `dite` structures.
More concisely: For any decidable proposition P and a two-argument function f, the application of f to dependent if-then-else constructs dite(h, t, e) is equivalent to dite(h, f(h), f(e)).
|
Mathlib.Logic.Basic._auxLemma.44
theorem Mathlib.Logic.Basic._auxLemma.44 : ∀ {p : Prop} {q : p → Prop}, ¬p → (∃ (h' : p), q h') = False
This theorem states that for any property `p` that depends on a truth value, asserting that this property holds for all truth values is equivalent to asserting that it holds for `True.intro`, the only instance of truth. Here, `True.intro` is Lean's way of representing the concept of 'true'. Essentially, this theorem is pointing out that if a property is always true, then it is specifically true for the value of 'true'.
More concisely: For any property `p`, `∀ (b : Bool), p b ≃ p True.intro`.
|
Mathlib.Logic.Basic._auxLemma.13
theorem Mathlib.Logic.Basic._auxLemma.13 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem states that for any two propositions `a` and `b`, the logical disjunction of `a` and `b` (denoted as `a ∨ b`) is equal to the disjunction of `b` and `a` (denoted as `b ∨ a`). In other words, in logic, the order of the operands in a disjunction does not matter, mirroring the commutative property in mathematics.
More concisely: For all propositions `a` and `b`, `a ∨ b` is equal to `b ∨ a` in Lean logic. (The logical disjunction of `a` and `b` is commutative.)
|
or_iff_not_and_not
theorem or_iff_not_and_not : ∀ {a b : Prop}, a ∨ b ↔ ¬(¬a ∧ ¬b)
This theorem states that for all propositions `a` and `b`, the statement "either `a` or `b` is true" is logically equivalent to the statement "it is not the case that both `a` and `b` are false". In mathematical terms, \(a \lor b\) is equivalent to \(\neg(\neg a \land \neg b)\). This is a basic result in propositional logic known as De Morgan's law.
More concisely: The logical equivalence of \(a \lor b\) and \(\neg(\neg a \land \neg b)\) holds in propositional logic.
|
And.rotate
theorem And.rotate : ∀ {a b c : Prop}, a ∧ b ∧ c → b ∧ c ∧ a
This theorem, referred to as "And.rotate", states that for any three propositions `a`, `b`, and `c`, if `a` and `b` and `c` are all true, then it follows that `b` and `c` and `a` are also true. In other words, it allows for the rotation of the positions of conjunctions in propositional logic.
More concisely: If propositions `a`, `b`, and `c` are all true, then so are `b`, `c`, and `a`.
|
Mathlib.Logic.Basic._auxLemma.10
theorem Mathlib.Logic.Basic._auxLemma.10 : ∀ {a b : Prop}, (a ∨ b) = (b ∨ a)
This theorem states that for any proposition `a`, the double negation of `a` is equivalent to `a`. In other words, not not `a` is the same as `a`. This is a fundamental theorem in classical logic, also known as the law of double negation.
More concisely: In classical logic, the double negation of a proposition `a` is equivalent to `a`.
|
by_cases
theorem by_cases : ∀ {p q : Prop}, (p → q) → (¬p → q) → q
This theorem, named `by_cases`, states that for any two propositions `p` and `q`, if `q` can be deduced from both `p` and the negation of `p` (`¬p`), then `q` must be true. In other words, regardless of whether `p` is true or false, if both cases imply the truth of `q`, then `q` is indeed true. This theorem is a formalization of the law of excluded middle in propositional logic.
More concisely: If `q` can be deduced from both `p` and `¬p`, then `q` is true. (This is the statement of the theorem named `by_cases` in Lean 4, representing the law of excluded middle in propositional logic.)
|
not_iff
theorem not_iff : ∀ {a b : Prop}, ¬(a ↔ b) ↔ (¬a ↔ b)
This theorem states that for any two propositions 'a' and 'b', the negation of the biconditional between 'a' and 'b' is equivalent to the biconditional between the negation of 'a' and 'b'. In other words, if 'a' is not equivalent to 'b', then 'b' is equivalent to the statement that 'a' is not true.
More concisely: The negation of (a ≤f/∥ b) is equivalent to (~a ≤f/∥ b) and (a ≤f/∥ b) is equivalent to (a ≤f/∥ ~b), where "≤f/∥" denotes biconditional.
|
forall₂_swap
theorem forall₂_swap :
∀ {ι₁ : Sort u_3} {ι₂ : Sort u_4} {κ₁ : ι₁ → Sort u_5} {κ₂ : ι₂ → Sort u_6}
{p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop},
(∀ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) ↔
∀ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂
This theorem, `forall₂_swap`, states that for any two sorts `ι₁` and `ι₂`, and any two functions `κ₁` and `κ₂` mapping from `ι₁` and `ι₂` respectively to other sorts, and a proposition `p` that relates elements from each sort, the proposition `p` holds for all combinations of elements of `ι₁` and `ι₂` irrespective of the order in which we choose the elements. That is, choosing an element from `ι₁` then `ι₂` is the same as choosing an element from `ι₂` then `ι₁`, as far as the proposition `p` is concerned.
More concisely: For any sorts `ι₁` and `ι₂` and functions `κ₁ : ι₁ → Sort`, `κ₂ : ι₂ → Sort`, and proposition `p : ∀ i₁ i₂, p (κ₁ i₁) (κ₂ i₂) ↔ p (κ₂ i₂) (κ₁ i₁)`, `p` is a symmetric relation between the images of `κ₁` and `κ₂`.
|
Exists.snd
theorem Exists.snd : ∀ {b : Prop} {p : b → Prop} (h : Exists p), p ⋯
This theorem, `Exists.snd`, states that for every property `p` dependent on a proposition `b` and for any proof `h` that there exists some element satisfying the property `p`, the property `p` holds true. In terms of logic, it's stating that if there is an existence proof of a particular property, then that property is indeed valid.
More concisely: If there exists an element with property `p` in a proposition `b`, then `p` holds for that element.
|
imp_iff_not_or
theorem imp_iff_not_or : ∀ {a b : Prop}, a → b ↔ ¬a ∨ b
This theorem states that for any two propositions `a` and `b`, the implication `a → b` is logically equivalent to `¬a ∨ b`. In other words, "if `a` then `b`" is the same as "either `a` is not true, or `b` is true". This is a principle from propositional logic.
More concisely: The logical equivalence of `a → b` and `¬a ∨ b` holds in propositional logic.
|
Membership.mem.ne_of_not_mem'
theorem Membership.mem.ne_of_not_mem' :
∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {s t : β} {a : α}, a ∈ s → a ∉ t → s ≠ t
This theorem, named `Membership.mem.ne_of_not_mem'`, states that for any types `α` and `β` with a defined `Membership` relation, and any elements `s` and `t` of `β` and `a` of `α`, if `a` is a member of `s` and is not a member of `t`, then `s` and `t` are not equal. Essentially, it asserts that two sets are unequal if there is an element that is contained in one set and not in the other.
More concisely: For all types `α` and `β` with a defined Membership relation, and for all `a : α` and `s`, `t : β`, if `a` is a member of `s` and not a member of `t`, then `s ≠ t`.
|
Function.mtr
theorem Function.mtr : ∀ {a b : Prop}, (¬a → ¬b) → b → a
This theorem, `Function.mtr`, states that for any two propositions `a` and `b`, if the negation of `a` implies the negation of `b`, then the truth of `b` implies the truth of `a`. In other words, given the implication (¬a → ¬b), and assuming `b` is true, we can deduce that `a` must also be true. This can be seen as a reverse form of modus tollens, hence the name `mtr`.
More concisely: If `a` implies `b` in logic (`a → b`), then the negation of `b` implies the negation of `a` (`¬b → ¬a`).
|
Not.imp_symm
theorem Not.imp_symm : ∀ {a b : Prop}, (¬a → b) → ¬b → a
This theorem states that for any two propositions `a` and `b`, if `b` is true whenever `a` is not true (expressed as `(¬a → b)`), then if `b` is not true (expressed as `¬b`), `a` must be true. In simpler terms, if the truth of `b` relies on the falsehood of `a`, then the falsehood of `b` guarantees the truth of `a`.
More concisely: If `(¬a → b)`, then `(¬b → a)`. In other words, the implication `a → b` is logically equivalent to the implication `¬b → a`.
|
Iff.and
theorem Iff.and : ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∧ b ↔ c ∧ d)
This theorem, `Iff.and`, states that for any four properties `a`, `b`, `c` and `d`, if `a` is logically equivalent to `c` and `b` is logically equivalent to `d`, then the conjunction `a ∧ b` is logically equivalent to the conjunction `c ∧ d`. In other words, if the logical relationships between `a` and `c` and between `b` and `d` are preserved, then the same holds for their conjunctions.
More concisely: If `a` is logically equivalent to `c` and `b` is logically equivalent to `d`, then `a ∧ b` is logically equivalent to `c ∧ d`.
|
Function.mt
theorem Function.mt : ∀ {a b : Prop}, (a → b) → ¬b → ¬a
This theorem, named `Function.mt`, establishes the principle of modus tollens for logical implications in the context of mathematical propositions. In more detail, for any two propositions `a` and `b`, it states that if `a` implies `b` and `b` is not true (denoted by `¬b`), then `a` must also not be true (denoted by `¬a`). This is a fundamental theorem in propositional logic.
More concisely: If `a` implies `b` and not `b`, then not `a`.
|
not_imp_comm
theorem not_imp_comm : ∀ {a b : Prop}, ¬a → b ↔ ¬b → a
This theorem states that for any two propositions 'a' and 'b', the statement "not 'a' implies 'b'" is logically equivalent to the statement "not 'b' implies 'a'". In other words, if we have a situation where the non-existence or falseness of 'a' guarantees the existence or truth of 'b', then we must also have the situation where the non-existence or falseness of 'b' guarantees the existence or truth of 'a', and vice versa.
More concisely: The negations of propositions 'a' and 'b' are logically equivalent: ~a <\imeq> b <=> ~b <\imeq> a.
|
not_ne_iff
theorem not_ne_iff : ∀ {α : Sort u_1} {a b : α}, ¬a ≠ b ↔ a = b
This theorem, `not_ne_iff`, states that for any type `α` and any two elements `a` and `b` of this type, the negation of `a` being not equal to `b` is logically equivalent to `a` being equal to `b`. This essentially captures the intuitive idea that if it's not true that some `a` is not equal to some `b`, then `a` must be equal to `b`. This holds in general for any type `α`.
More concisely: For all types `α` and elements `a` and `b` of type `α`, `a ≠ b` is logically equivalent to `a = b`.
|
xor_true
theorem xor_true : Xor' True = Not
The theorem `xor_true` states that the exclusive or function `Xor'` applied to the proposition `True` is equivalent to the negation function `Not`. In other words, if either of two propositions is true, but not both, and one of those propositions is `True`, this is equivalent to saying that the other proposition is false.
More concisely: The theorem `xor_true` asserts that `Xor' True False ≡ Not False`.
|
exists_prop_congr'
theorem exists_prop_congr' :
∀ {p p' : Prop} {q q' : p → Prop}, (∀ (h : p), q h ↔ q' h) → ∀ (hp : p ↔ p'), Exists q = ∃ (h : p'), q' ⋯ := by
sorry
This theorem states that for any propositions `p` and `p'`, and for any properties `q` and `q'` that depend on `p`, if for all `h` in `p`, `q h` is equivalent to `q' h`, and if `p` is equivalent to `p'`, then there exists an `h` in `p` such that `q h` is true if and only if there exists an `h` in `p'` such that `q' h` is true. The theorem thus establishes a congruence relationship for existential quantifiers under certain conditions of proposition and property equivalence.
More concisely: If propositions `p` and `p'` are equivalent, and for all `h` in `p`, properties `q(h)` and `q'(h)` are equivalent, then there exists a common element `h` in `p` and `p'` such that `q(h)` if and only if `q'(h)` is true.
|