latte-sets.algebra
The boolean algebra operators for sets.
comp-empty-full
(comp-empty-full [T :type])(seteq (complement (emptyset T)) (fullset T))
Theorem:
comp-full-empty
(comp-full-empty [T :type])(seteq (complement (fullset T)) (emptyset T))
Theorem:
complement
(complement [s (set T)])(set-of [x T] (not (elem x s)))
Definition: The complement of set s.
Note that the definition is more self-contained in type theory than with classical sets. The complement is here wrt. a type T which is well defined, wherease in classical set theory one has to introduce a somewhat unsatisfying notion of “a universe of discourse”.
diff
(diff [s1 (set T)] [s2 (set T)])(lambda [x T] (and (elem x s1) (not (elem x s2))))
Definition: Set difference
(difference T s1 s2) is the set s1∖s2.
diff-cancel
(diff-cancel [s (set T)])(seteq (diff s s) (emptyset T))
Theorem:
diff-empty-left
(diff-empty-left [s (set T)])(seteq (diff (emptyset T) s) (emptyset T))
Theorem:
diff-empty-right
(diff-empty-right [s (set T)])(seteq (diff s (emptyset T)) s)
Theorem:
dist-inter-union
(dist-inter-union [s1 (set T)] [s2 (set T)] [s3 (set T)])(seteq (inter s1 (union s2 s3)) (union (inter s1 s2) (inter s1 s3)))
Theorem: Distributivity of intersection over union.
dist-inter-union-sym
(dist-inter-union-sym [s1 (set T)] [s2 (set T)] [s3 (set T)])(seteq (union (inter s1 s2) (inter s1 s3)) (inter s1 (union s2 s3)))
Theorem: Symmetric case of dist-inter-union.
dist-union-inter
(dist-union-inter [s1 (set T)] [s2 (set T)] [s3 (set T)])(seteq (union s1 (inter s2 s3)) (inter (union s1 s2) (union s1 s3)))
Theorem: Distributivity of union over intersection.
dist-union-inter-sym
(dist-union-inter-sym [s1 (set T)] [s2 (set T)] [s3 (set T)])(seteq (inter (union s1 s2) (union s1 s3)) (union s1 (inter s2 s3)))
Theorem: Symmetric case of dist-union-inter.
inter
(inter [s1 (set T)] [s2 (set T)])(lambda [x T] (and (elem x s1) (elem x s2)))
Definition: Set intersection, i.e. the set s1∩s2.
inter-assoc
(inter-assoc [s1 (set T)] [s2 (set T)] [s3 (set T)])(seteq (inter s1 (inter s2 s3)) (inter (inter s1 s2) s3))
Theorem:
inter-assoc-sym
(inter-assoc-sym [s1 (set T)] [s2 (set T)] [s3 (set T)])(seteq (inter (inter s1 s2) s3) (inter s1 (inter s2 s3)))
Theorem:
inter-commute
(inter-commute [s1 (set T)] [s2 (set T)])(seteq (inter s1 s2) (inter s2 s1))
Theorem: Set intersection commutes.
inter-elim-left
(inter-elim-left [s1 (set T)] [s2 (set T)] [x T])(==> (elem x (inter s1 s2)) (elem x s1))
Theorem: Elimination rule for intersection (left operand).
inter-elim-right
(inter-elim-right [s1 (set T)] [s2 (set T)] [x T])(==> (elem x (inter s1 s2)) (elem x s2))
Theorem: Elimination rule for intersection (right operand).
inter-empty
(inter-empty [s (set T)])(seteq (inter s (emptyset T)) (emptyset T))
Theorem:
inter-idem
(inter-idem [s (set T)])(seteq (inter s s) s)
Theorem:
symdiff
(symdiff [s1 (set T)] [s2 (set T)])(lambda
[x T]
(or
(and (elem x s1) (not (elem x s2)))
(and (elem x s2) (not (elem x s1)))))
Definition: Symmetric difference, often denoted by s1∆s2.
symdiff-alt
(symdiff-alt [s1 (set T)] [s2 (set T)])(seteq (symdiff s1 s2) (union (diff s1 s2) (diff s2 s1)))
Theorem: An alternative caracterisation of the symmetric difference.
union
(union [s1 (set T)] [s2 (set T)])(lambda [x T] (or (elem x s1) (elem x s2)))
Definition: Set union, (union s1 s2) is the set s1∪s2.
union-assoc
(union-assoc [s1 (set T)] [s2 (set T)] [s3 (set T)])(seteq (union s1 (union s2 s3)) (union (union s1 s2) s3))
Theorem:
union-assoc-sym
(union-assoc-sym [s1 (set T)] [s2 (set T)] [s3 (set T)])(seteq (union (union s1 s2) s3) (union s1 (union s2 s3)))
Theorem:
union-commute
(union-commute [s1 (set T)] [s2 (set T)])(seteq (union s1 s2) (union s2 s1))
Theorem: Set union commutes.
union-empty
(union-empty [s (set T)])(seteq (union s (emptyset T)) s)
Theorem:
union-idem
(union-idem [s (set T)])(seteq (union s s) s)
Theorem: