Revision #1324 → #2031 · back to history
modifiedExistential implies negated universal542ecb4ec103
| Field | From #1324 | To #2031 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.PropLemmas |
modifiedImport-export equivalenceb9ce542c4dfb
| Field | From #1324 | To #2031 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.SimpLemmas |
modifiedExcluded middle equivalent to consequentia mirabilisce62e02f7e2a
| Field | From #1324 | To #2031 |
|---|
| note | Consequentia mirabilis is not named or formalized in Mathlib (grep for `consequentia`/`mirabilis` returned no Mathlib hits). | Consequentia mirabilis is not named or formalized in Mathlib (loogle for `consequentia` returned 0 hits). |
modifiedEquivalence as conjunction of implicationse72218c8f577
| Field | From #1324 | To #2031 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Core |
modifiedValidity of ¬(A ∧ ¬A)46f88686871d
| Field | From #1324 | To #2031 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.PropLemmas |
| note | `¬(A ∧ ¬A)` is provable intuitionistically; Mathlib has `not_and_self` and a Heyting-algebra analogue `inf_compl_eq_bot`. | `¬(A ∧ ¬A)` is provable intuitionistically; Mathlib has `not_and_self_iff` and a Heyting-algebra analogue `inf_compl_eq_bot`. |
addedPrinciple of explosion9edfdf3ad463
addedLaw of non-contradiction16cc0f3b8395
addedDrinker's paradoxf0f663df3149
addedDisjunctive syllogism2f37f6b20fcf
addedReverse law of contrapositiond2aa38f97ee4
addedCurry/uncurry as conjunction–implication equivalence2921f1fe4442
addedNegation introduction via implication of contradiction3b8de9de7ef7