mirror of
https://github.com/tomasriveral/ZeroToLean.git
synced 2026-08-11 18:28:39 +02:00
31 lines
1.9 KiB
Markdown
31 lines
1.9 KiB
Markdown
### Basic logic
|
|
|
|
| Name | Mathlib equivalent | Proposition |
|
|
|---------------|--------------------|-------------|
|
|
|`basicLogic.and_commutative` | `and_comm` | $$a\land b \iff b \land a$$ |
|
|
|`basicLogic.or_commutative` | `or_comm` | $$a\lor b \iff b \lor a$$ |
|
|
|`basicLogic.double_negation` | `not_not_intro` | $$a\to\neg\neg a$$ |
|
|
|`basicLogic.and_associative` | `and_assoc` | $$a\land (b\land c) \iff (a\land b) \land c$$ |
|
|
|`basicLogic.contrapositive` | `contrapose` | $$(a \to b) \to (\neg b \to \neg a)$$ |
|
|
|`basicLogic.p_or_p_equal_p` | `or_self` | $$(a \lor a) = a$$ |
|
|
|`basicLogic.p_or_p_iff_p` | | $$a \lor a \iff a$$ |
|
|
|`basicLogic.and_or_distributivity_left` | `and_or_left` | $$a \land (b \lor c) \iff (a \land b) \lor (a \land c)$$ |
|
|
|`basicLogic.and_or_distributivity_right` | `and_or_right` | $$(a \land b) \lor c \iff (a \lor c) \land (b \lor c)$$ |
|
|
|`basicLogic.p_and_true_equal_p` | `and_true` | $$(a \land True) = a$$ |
|
|
|`basicLogic.p_and_true_iff_p` | | $$a \land True \iff a$$ |
|
|
|`basicLogic.true_and_p_equal_p` | `true_and` | $$(True \land a) = a$$ |
|
|
|`basicLogic.true_and_p_iff_p` | | $$True \land a \iff a$$ |
|
|
|`basicLogic.p_or_false_equal_p` | `or_false` | $$(a \lor False) = a$$ |
|
|
|`basicLogic.p_or_false_iff_p` | | $$a \lor False \iff a$$ |
|
|
|`basicLogic.false_or_p_equal_p` | `false_or` | $$(False \lor a) = a$$ |
|
|
|`basicLogic.false_or_p_iff_p` | | $$False \lor a \iff a$$ |
|
|
|`basicLogic.and_false_equal_false` | `and_false` | $$(a \land False) = False$$ |
|
|
|`basicLogic.and_false_iff_false` | | $$a \land False \iff False$$ |
|
|
|`basicLogic.false_and_equal_false` | `false_and` | $$(False \land a) = False$$ |
|
|
|`basicLogic.false_and_iff_false` | | $$False \land a \iff False$$ |
|
|
|`basicLogic.or_true_equal_true` | `or_true` | $$(a \lor True) = True$$ |
|
|
|`basicLogic.or_true_iff_true` | | $$a \lor True \iff True$$ |
|
|
|`basicLogic.true_or_equal_true` | `true_or` | $$(True \lor a) = True$$ |
|
|
|`basicLogic.true_or_iff_true` | | $$True \lor a \iff True$$ |
|
|
|