These are theorems in the Boolean algebra document.
Chris Pressey
1 year, 2 months ago
| 170 | 170 | Before we state the other De Morgan's law, we state a couple of other |
| 171 | 171 | useful lemmas involving `not`. |
| 172 | 172 | |
| 173 | theorem | |
| 173 | theorem (#comp-universe) | |
| 174 | 174 | not(1) = 0 |
| 175 | 175 | proof |
| 176 | 176 | 0 = 0 |
| 180 | 180 | not(1) = 0 |
| 181 | 181 | qed |
| 182 | 182 | |
| 183 | theorem | |
| 183 | theorem (#comp-empty) | |
| 184 | 184 | not(0) = 1 |
| 185 | 185 | proof |
| 186 | 186 | 1 = 1 |
| 27 | 27 | |
| 28 | 28 | Requires [Set Difference](set-difference.eqthy.md) |
| 29 | 29 | (which itself is based on [Boolean algebra](boolean-algebra.md)). |
| 30 | ||
| 31 | // TODO: these should be from boolean algebra | |
| 32 | axiom (#comp-universe) not(1) = 0 | |
| 33 | axiom (#comp-empty) not(0) = 1 | |
| 34 | 30 | |
| 35 | 31 | axiom (#interior-closed) diff(interior(X), X) = 0 |
| 36 | 32 | axiom (#interior-idem) interior(interior(X)) = interior(X) |