Revision #3555 → #4112 · back to history
modifiedPrinciple of bivalence and law of excluded middlea715ad04c114
| Field | From #3555 | To #4112 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
modifiedTruth of negation (¬ semantics)660bb6beb891
| Field | From #3555 | To #4112 |
|---|
| mathlib.decl | not_not | Classical.not_not |
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
| note | Classical double negation `¬¬p ↔ p` (`not_not`, re-exported from `Classical`) is a key consequence of the classical truth-of-negation clause; the meta-level assignment clause itself is not a Mathlib decl. | Classical double negation `¬¬p ↔ p` (`Classical.not_not`) is a key consequence of the classical truth-of-negation clause; the meta-level assignment clause itself is not a Mathlib decl. |
modifiedDouble negation985a50e62f11
| Field | From #3555 | To #4112 |
|---|
| mathlib.decl | not_not | Classical.not_not |
| mathlib.module | Mathlib.Logic.Basic | Init.Classical |
| note | Classical double negation elimination `¬¬p ↔ p` is `not_not` (re-exported from `Classical.not_not`) in Mathlib. | Classical double negation elimination `¬¬p ↔ p` is `Classical.not_not` in Lean core (used throughout Mathlib). |
addedConjunction introduction and elimination23288130d538
addedDisjunction introduction and eliminationf50a5f1fb305
addedBiconditional introduction and eliminationea3ae7cbeb66
addedImplication introduction and elimination (modus ponens)05356282f775
addedTautology (idempotence of ∧ and ∨)7b8d97a1c8fe
addedAbsorption laws3fec441ae97c