| 8 | 8 |
|
| 9 | 9 |
Some theorems about set difference.
|
| 10 | 10 |
|
| 11 | |
Using the [Algebra of sets (Wikipedia)](https://en.wikipedia.org/wiki/Algebra_of_sets)
|
| 12 | |
as a basis. (TODO: just change to using Boolean algebra as the basis.)
|
|
11 |
These theorems, as usually stated, are based on an [Algebra of sets (Wikipedia)](https://en.wikipedia.org/wiki/Algebra_of_sets).
|
|
12 |
However, we will use Boolean algebra as their basis here. (I'm given to
|
|
13 |
understand that these two theories are subtlely different, but I've concluded
|
|
14 |
that the difference, if there is one, is too subtle to matter for our purposes;
|
|
15 |
all the axioms and properties we care about are shared by the two,
|
|
16 |
and it is only a matter of adjusting the nomenclature.)
|
| 13 | 17 |
|
| 14 | |
Requires [Algebra of Sets](algebra-of-sets.eqthy.md).
|
| 15 | |
|
| 16 | |
axiom (#union-de-morg) comp(inter(A, B)) = union(comp(A), comp(B))
|
| 17 | |
axiom (#inter-de-morg) comp(union(A, B)) = inter(comp(A), comp(B))
|
|
18 |
Requires [Boolean algebra](boolean-algebra.eqthy.md).
|
| 18 | 19 |
|
| 19 | 20 |
Definition of set difference.
|
| 20 | 21 |
|
| 21 | |
axiom (#diff) diff(A, B) = inter(A, comp(B))
|
|
22 |
axiom (#diff) diff(A, B) = and(A, not(B))
|
| 22 | 23 |
|
| 23 | 24 |
A theorem about set difference: difference distributes over union.
|
| 24 | 25 |
|
| 25 | 26 |
theorem (#diff-union-distrib)
|
| 26 | |
union(diff(A, C), diff(B, C)) = diff(union(A, B), C)
|
|
27 |
or(diff(A, C), diff(B, C)) = diff(or(A, B), C)
|
| 27 | 28 |
proof
|
| 28 | |
union(diff(A, C), diff(B, C)) = union(diff(A, C), diff(B, C))
|
| 29 | |
union(diff(A, C), diff(B, C)) = union(diff(A, C), inter(B, comp(C)))
|
| 30 | |
union(diff(A, C), diff(B, C)) = union(inter(A, comp(C)), inter(B, comp(C)))
|
| 31 | |
union(diff(A, C), diff(B, C)) = union(inter(A, comp(C)), inter(comp(C), B))
|
| 32 | |
union(diff(A, C), diff(B, C)) = union(inter(comp(C), A), inter(comp(C), B))
|
| 33 | |
union(diff(A, C), diff(B, C)) = inter(comp(C), union(A, B))
|
| 34 | |
union(diff(A, C), diff(B, C)) = inter(union(A, B), comp(C))
|
| 35 | |
union(diff(A, C), diff(B, C)) = diff(union(A, B), C)
|
|
29 |
or(diff(A, C), diff(B, C)) = or(diff(A, C), diff(B, C))
|
|
30 |
or(diff(A, C), diff(B, C)) = or(diff(A, C), and(B, not(C)))
|
|
31 |
or(diff(A, C), diff(B, C)) = or(and(A, not(C)), and(B, not(C)))
|
|
32 |
or(diff(A, C), diff(B, C)) = or(and(A, not(C)), and(not(C), B))
|
|
33 |
or(diff(A, C), diff(B, C)) = or(and(not(C), A), and(not(C), B))
|
|
34 |
or(diff(A, C), diff(B, C)) = and(not(C), or(A, B))
|
|
35 |
or(diff(A, C), diff(B, C)) = and(or(A, B), not(C))
|
|
36 |
or(diff(A, C), diff(B, C)) = diff(or(A, B), C)
|
| 36 | 37 |
qed
|
| 37 | 38 |
|
| 38 | |
Another theorem about set difference. This one uses De Morgan's law, which
|
| 39 | |
has been added as an axiom above. For a working-out of it, see the
|
| 40 | |
Boolean algebra document.
|
|
39 |
Another theorem about set difference: the difference of A and B is the
|
|
40 |
same as the difference of A and the intersection of A and B.
|
| 41 | 41 |
|
| 42 | 42 |
theorem (#diff-of-inter-is-diff)
|
| 43 | |
diff(A, B) = diff(A, inter(A, B))
|
|
43 |
diff(A, B) = diff(A, and(A, B))
|
| 44 | 44 |
proof
|
| 45 | 45 |
diff(A, B) = diff(A, B)
|
| 46 | |
diff(A, B) = inter(A, comp(B))
|
| 47 | |
diff(A, B) = union(inter(A, comp(B)), e)
|
| 48 | |
diff(A, B) = union(e, inter(A, comp(B)))
|
| 49 | |
diff(A, B) = union(inter(A, comp(A)), inter(A, comp(B)))
|
| 50 | |
diff(A, B) = inter(A, union(comp(A), comp(B)))
|
| 51 | |
diff(A, B) = inter(A, comp(inter(A, B)))
|
| 52 | |
diff(A, B) = diff(A, inter(A, B))
|
|
46 |
diff(A, B) = and(A, not(B))
|
|
47 |
diff(A, B) = or(and(A, not(B)), 0)
|
|
48 |
diff(A, B) = or(0, and(A, not(B)))
|
|
49 |
diff(A, B) = or(and(A, not(A)), and(A, not(B)))
|
|
50 |
diff(A, B) = and(A, or(not(A), not(B)))
|
|
51 |
diff(A, B) = and(A, not(and(A, B)))
|
|
52 |
diff(A, B) = diff(A, and(A, B))
|
| 53 | 53 |
qed
|
| 54 | 54 |
|
| 55 | 55 |
Both of these theorems were adapted from
|