Classical.choose_spec
theorem Classical.choose_spec : ∀ {α : Sort u} {p : α → Prop} (h : ∃ x, p x), p (Classical.choose h)
The theorem `Classical.choose_spec` states that for any type `α` and any property `p` that holds for some element of `α`, the element chosen by the function `Classical.choose` from the existence proof `h` also satisfies the property `p`. In other words, if there exists an element `x` of type `α` for which property `p` holds, then the property `p` will hold for the element returned by `Classical.choose` when called with the proof of this existence.
More concisely: If `p` is a property that holds for some element of type `α`, then the element returned by `Classical.choose` from an existence proof of `p` also satisfies `p`.
|
Classical.skolem
theorem Classical.skolem :
∀ {α : Sort u} {b : α → Sort v} {p : (x : α) → b x → Prop}, (∀ (x : α), ∃ y, p x y) ↔ ∃ f, ∀ (x : α), p x (f x)
This theorem, referred to as Skolem's theorem, states that for any type `α`, any type function `b` from `α` to another type, and any predicate `p` over `α` and `b x`, the assertion that for every element of type `α` there exists an element of type `b x` such that the predicate `p` holds, is equivalent to the existence of a function `f` from `α` to `b x` such that the predicate `p` holds for every `x` and `f x`. In other words, this theorem captures the idea that universal quantification over a type followed by existential quantification over another type can be switched to existential quantification over a function followed by universal quantification over the first type, provided the predicate holds. This is essentially a formal statement of the Skolem's theorem in the context of mathematical logic and first-order theories.
More concisely: Skolem's theorem states that given a type `α`, a type function `b`, and a predicate `p`, the existence of a function `f` from `α` to `b` such that `p(x, f(x))` holds for all `x` in `α` is equivalent to the existence of an element in `b` for every `x` in `α` satisfying `p(x, y)`.
|
Exists.choose_spec
theorem Exists.choose_spec : ∀ {α : Sort u_1} {p : α → Prop} (P : ∃ a, p a), p P.choose
The theorem `Exists.choose_spec` states that for any propositional function `p` on elements of type `α` and for any existential statement `P` of the form "there exists an element `a` such that `p(a)` is true", the element extracted from this existential statement `P` using the function `Exists.choose` satisfies the property `p`. In other words, if `P` is a proof of existence of an element satisfying `p`, then `p` holds for `Exists.choose P`.
More concisely: For any propositional function `p` and existential statement "there exists an element `a` of type `α` such that `p(a)` holds, the extracted element `Exists.choose (exists a, p a)` satisfies `p`.
|
Classical.em
theorem Classical.em : ∀ (p : Prop), p ∨ ¬p
**Diaconescu's Theorem**: This theorem states that for any proposition `p`, either `p` or `not p` holds true. This is the principle of the excluded middle, which is derived from the axiom of choice, function extensionality, and propositional extensionality. In other words, it asserts that any proposition is either true or its negation is true, leaving no room for a proposition to exist in a state of uncertainty or ambiguity.
More concisely: For any proposition `p` in Lean 4 logic, either `p` or `not p` holds.
|
Classical.byContradiction
theorem Classical.byContradiction : ∀ {p : Prop}, (¬p → False) → p
This theorem, `Classical.byContradiction`, states that for any proposition `p`, if assuming the negation of `p` leads to a contradiction (expressed as `¬p → False`), then `p` must be true. This corresponds to the classical logic principle of proof by contradiction (also known as reductio ad absurdum), where you prove a statement to be true by showing that its negation would result in an unreasonable or impossible situation.
More concisely: If assuming the negation of a proposition leads to a contradiction, then the proposition is true.
|
Classical.not_not
theorem Classical.not_not : ∀ {a : Prop}, ¬¬a ↔ a
This is the Double Negation Theorem. It states that for any proposition `a`, the double negation `¬¬a` is equivalent to `a`. The theorem further explains that the implication from `¬¬a` to `a`, also known as double negation elimination (DNE), is universally true in classical logic, but not in constructive logic.
More concisely: In classical logic, the double negation of a proposition is equivalent to the proposition itself.
|
Classical.axiomOfChoice
theorem Classical.axiomOfChoice :
∀ {α : Sort u} {β : α → Sort v} {r : (x : α) → β x → Prop}, (∀ (x : α), ∃ y, r x y) → ∃ f, ∀ (x : α), r x (f x)
This theorem, referred to as the 'axiom of choice', states that for any types `α` and `β` that depend on `α`, and a property `r` that relates an instance of `α` to an instance of `β`, if for every instance of `α` there exists an instance of `β` that satisfies the property `r`, then there exists a function `f` from `α` to `β` such that for each instance of `α`, the corresponding instance of `β` via function `f` satisfies the property `r`.
In mathematical terms, given a family of nonempty sets (indexed by α), there exists a function that can select one member from each of these sets such that a particular property holds. This is a fundamental concept in set theory and has profound implications in many areas of mathematics.
More concisely: The axiom of choice asserts that for any family of nonempty sets indexed by a type `α`, there exists a function that maps each instance of `α` to a distinct element in the corresponding set, such that the image under this function of each instance satisfies a given property.
|
Classical.epsilon_spec
theorem Classical.epsilon_spec : ∀ {α : Sort u} {p : α → Prop} (hex : ∃ y, p y), p (Classical.epsilon p)
This theorem, `Classical.epsilon_spec`, states that for any type `α` and any property `p` from `α` to `Prop`, if there exists an element `y` of `α` that satisfies the property `p`, then the Hilbert epsilon function applied to the property `p` also satisfies the property `p`. In other words, if there is an `y` such that `p(y)` is true, then `p(Classical.epsilon p)` is also true. This theorem is a key property of the Hilbert epsilon function, which chooses an arbitrary element that satisfies a given property if such an element exists.
More concisely: If a property `p` of type `α` has an element `y` satisfying it, then the Hilbert epsilon function `Classical.epsilon p` also satisfies `p`.
|