Classical.prop_complete
theorem Classical.prop_complete : ∀ (a : Prop), a = True ∨ a = False
This theorem, named `Classical.prop_complete`, asserts that for any proposition `a`, it must be the case that `a` is either equivalent to `True` or `False`. In other words, it states the law of the excluded middle in propositional logic, which says that any statement is either true or false and there are no other possibilities.
More concisely: For any proposition `a` in Lean 4 logic, `a` is equivalent to `True` or `False`.
|
Classical.by_cases
theorem Classical.by_cases : ∀ {p q : Prop}, (p → q) → (¬p → q) → q
This theorem, also known as the `Classical.by_cases`, states that for any propositions `p` and `q`, if `q` follows from `p` and `q` also follows from the negation of `p` (`¬p`), then `q` must be true. In simple terms, if `q` is true whether `p` is true or false, then `q` is absolutely true. This is a variant of the principle of excluded middle in classical logic.
More concisely: If `q` holds in both `p` and `¬p`, then `q` is a logical truth.
|
Classical.axiom_of_choice
theorem Classical.axiom_of_choice :
∀ {α : Sort u} {β : α → Sort v} {r : (x : α) → β x → Prop}, (∀ (x : α), ∃ y, r x y) → ∃ f, ∀ (x : α), r x (f x)
This theorem, `Classical.axiom_of_choice`, is an alias of the Axiom of Choice. In simple terms, it states that for any two types `α` and `β`, and a property `r` defined on these types, if for every element of type `α` there exists an element of type `β` such that the property `r` holds, then there exists a function `f` from `α` to `β` such that for every element of type `α`, the property `r` holds between `α` and `f(α)`. This is a fundamental principle in set theory and has important implications in many areas of mathematics.
More concisely: For any types `α` and `β` and property `r` on `α × β`, if for every `a ∈ α`, there exists `b ∈ β` such that `r(a, b)` holds, then there exists a function `f : α → β` such that for all `a ∈ α`, `r(a, f(a))` holds.
|
Classical.by_contradiction
theorem Classical.by_contradiction : ∀ {p : Prop}, (¬p → False) → p
This theorem, known as an "Alias" of `Classical.byContradiction`, states that for any proposition `p`, if the negation of `p` leads to a contradiction (i.e., is false), then `p` must be true. In other words, if assuming `p` is not true results in an impossible situation, then `p` has to be true. This is a fundamental principle in classical logic known as proof by contradiction.
More concisely: In classical logic, if the negation of a proposition leads to a contradiction, then the proposition is true.
|