Entry	Value
Package Name	set-thm
Count	246
Theorems	ABSORPTION : !x s. x IN s <=> x INSERT s = s BIJECTIVE_LEFT_RIGHT_INVERSE : !f. (!x y. f x = f y ==> x = y) /\ (!y. ?x. f x = y) <=> (?g. (!y. f (g y) = y) /\ (!x. g (f x) = x)) BIJECTIVE_ON_LEFT_RIGHT_INVERSE : !f s t. (!x. x IN s ==> f x IN t) ==> ((!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\ (!y. y IN t ==> (?x. x IN s /\ f x = y)) <=> (?g. (!y. y IN t ==> g y IN s) /\ (!y. y IN t ==> f (g y) = y) /\ (!x. x IN s ==> g (f x) = x))) COMPONENT : !x s. x IN x INSERT s CROSS_EMPTY : !s. s CROSS {} = {} CROSS_EQ_EMPTY : !s t. s CROSS t = {} <=> s = {} \/ t = {} CROSS_UNIV : UNIV CROSS UNIV = UNIV DECOMPOSITION : !s x. x IN s <=> (?t. s = x INSERT t /\ ~(x IN t)) DELETE_COMM : !x y s. s DELETE x DELETE y = s DELETE y DELETE x DELETE_DELETE : !x s. s DELETE x DELETE x = s DELETE x DELETE_DIFF_SING : !x s. s DIFF {x} = s DELETE x DELETE_INSERT : !x y s. (x INSERT s) DELETE y = (if x = y then s DELETE y else x INSERT (s DELETE y)) DELETE_INSERT_NON_ELEMENT : !x s. (x INSERT s) DELETE x = s <=> ~(x IN s) DELETE_INTER : !s t x. s DELETE x INTER t = (s INTER t) DELETE x DELETE_NON_ELEMENT : !x s. s DELETE x = s <=> ~(x IN s) DELETE_SUBSET : !x s. s DELETE x SUBSET s DIFF_COMM : !t u s. s DIFF t DIFF u = s DIFF u DIFF t DIFF_DIFF : !s t. s DIFF t DIFF t = s DIFF t DIFF_EMPTY : !s. s DIFF {} = s DIFF_EMPTY_SUBSET : !s t. s DIFF t = {} <=> s SUBSET t DIFF_EQ_EMPTY : !s. s DIFF s = {} DIFF_INSERT : !s t x. s DIFF x INSERT t = s DELETE x DIFF t DIFF_INTERS : !u s. u DIFF INTERS s = UNIONS {u DIFF t | t IN s} DIFF_SUBSET : !s t. s DIFF t SUBSET s DIFF_UNION : !t u s. s DIFF t DIFF u = s DIFF (t UNION u) DIFF_UNIONS : !u s. u DIFF UNIONS s = u INTER INTERS {u DIFF t | t IN s} DIFF_UNION_CANCEL : !s t. s DIFF t UNION t = s UNION t DIFF_UNION_SUBSET : !s t. t DIFF s UNION s = t <=> s SUBSET t DIFF_UNIV : !s. s DIFF UNIV = {} DISJOINT_DELETE_SYM : !s t x. DISJOINT (s DELETE x) t <=> DISJOINT (t DELETE x) s DISJOINT_DIFF : !s t. s DIFF t = s <=> DISJOINT s t DISJOINT_DIFF1 : !s t. DISJOINT (t DIFF s) s DISJOINT_DIFF2 : !s t. DISJOINT s (t DIFF s) DISJOINT_EMPTY : !s. DISJOINT s {} DISJOINT_EMPTY_REFL : !s. DISJOINT s s <=> s = {} DISJOINT_INSERT : !x s t. DISJOINT (x INSERT s) t <=> ~(x IN t) /\ DISJOINT s t DISJOINT_SING : !x s. DISJOINT s {x} <=> ~(x IN s) DISJOINT_SYM : !s t. DISJOINT s t <=> DISJOINT t s DISJOINT_UNION : !s t u. DISJOINT (s UNION t) u <=> DISJOINT s u /\ DISJOINT t u DISJOINT_UNIONS : !s t. DISJOINT s (UNIONS t) <=> (!x. x IN t ==> DISJOINT s x) EMPTY_CROSS : !s. {} CROSS s = {} EMPTY_DELETE : !x. {} DELETE x = {} EMPTY_DIFF : !s. {} DIFF s = {} EMPTY_DISJOINT : !s. DISJOINT {} s EMPTY_FUNSPACE : !d t. {f | (!x. x IN {} ==> f x IN t) /\ (!x. ~(x IN {}) ==> f x = d)} = {(\x. d)} EMPTY_GSPEC : GSPEC (\x. F) = {} EMPTY_NUMSEG_LT : {m | m < 0} = {} EMPTY_POWERSET : {s | s SUBSET {}} = {{}} EMPTY_PRODUCT_DEPENDENT : !t. {x,y | x IN {} /\ y IN t x} = {} EMPTY_SUBSET : !s. {} SUBSET s EMPTY_UNION : !s t. s UNION t = {} <=> s = {} /\ t = {} EMPTY_UNIONS : !s. UNIONS s = {} <=> (!t. t IN s ==> t = {}) EQ_UNIV : !s. (!x. x IN s) <=> s = UNIV EXISTS_IN_GSPEC1 : !p f q. (?z. z IN {f x | p x} /\ q z) <=> (?x. p x /\ q (f x)) EXISTS_IN_GSPEC2 : !p f q. (?z. z IN {f x y | p x y} /\ q z) <=> (?x y. p x y /\ q (f x y)) EXISTS_IN_GSPEC3 : !p f q. (?z. z IN {f w x y | p w x y} /\ q z) <=> (?w x y. p w x y /\ q (f w x y)) EXISTS_IN_IMAGE : !p f s. (?y. y IN IMAGE f s /\ p y) <=> (?x. x IN s /\ p (f x)) EXISTS_IN_INSERT : !p a s. (?x. x IN a INSERT s /\ p x) <=> p a \/ (?x. x IN s /\ p x) EXISTS_IN_UNION : !p s t. (?x. x IN s UNION t /\ p x) <=> (?x. x IN s /\ p x) \/ (?x. x IN t /\ p x) EXISTS_IN_UNIONS : !p s. (?x. x IN UNIONS s /\ p x) <=> (?t x. t IN s /\ x IN t /\ p x) EXISTS_SUBSET_IMAGE : !p f s. (?t. t SUBSET IMAGE f s /\ p t) <=> (?t. t SUBSET s /\ p (IMAGE f t)) EXISTS_SUBSET_IMAGE_INJ : !p f s. (?t. t SUBSET IMAGE f s /\ p t) <=> (?t. t SUBSET s /\ (!x y. x IN t /\ y IN t /\ f x = f y ==> x = y) /\ p (IMAGE f t)) EXISTS_SUBSET_INSERT : !p x t. (?s. s SUBSET x INSERT t /\ p s) <=> (?s. s SUBSET t /\ (p s \/ p (x INSERT s))) EXISTS_SUBSET_UNION : !p t u. (?s. s SUBSET t UNION u /\ p s) <=> (?t' u'. t' SUBSET t /\ u' SUBSET u /\ p (t' UNION u')) EXTENSION' : !s t. (!x. x IN s <=> x IN t) <=> s = t FORALL_IN_GSPEC1 : !p f q. (!z. z IN {f x | p x} ==> q z) <=> (!x. p x ==> q (f x)) FORALL_IN_GSPEC2 : !p f q. (!z. z IN {f x y | p x y} ==> q z) <=> (!x y. p x y ==> q (f x y)) FORALL_IN_GSPEC3 : !p f q. (!z. z IN {f w x y | p w x y} ==> q z) <=> (!w x y. p w x y ==> q (f w x y)) FORALL_IN_IMAGE : !p f s. (!y. y IN IMAGE f s ==> p y) <=> (!x. x IN s ==> p (f x)) FORALL_IN_IMAGE_2 : !p f s. (!x y. x IN IMAGE f s /\ y IN IMAGE f s ==> p x y) <=> (!x y. x IN s /\ y IN s ==> p (f x) (f y)) FORALL_IN_INSERT : !p a s. (!x. x IN a INSERT s ==> p x) <=> p a /\ (!x. x IN s ==> p x) FORALL_IN_UNION : !p s t. (!x. x IN s UNION t ==> p x) <=> (!x. x IN s ==> p x) /\ (!x. x IN t ==> p x) FORALL_IN_UNIONS : !p s. (!x. x IN UNIONS s ==> p x) <=> (!t x. t IN s /\ x IN t ==> p x) FORALL_SUBSET_IMAGE : !p f s. (!t. t SUBSET IMAGE f s ==> p t) <=> (!t. t SUBSET s ==> p (IMAGE f t)) FORALL_SUBSET_IMAGE_INJ : !p f s. (!t. t SUBSET IMAGE f s ==> p t) <=> (!t. t SUBSET s /\ (!x y. x IN t /\ y IN t /\ f x = f y ==> x = y) ==> p (IMAGE f t)) FORALL_SUBSET_INSERT : !p x t. (!s. s SUBSET x INSERT t ==> p s) <=> (!s. s SUBSET t ==> p s /\ p (x INSERT s)) FORALL_SUBSET_UNION : !p t u. (!s. s SUBSET t UNION u ==> p s) <=> (!t' u'. t' SUBSET t /\ u' SUBSET u ==> p (t' UNION u')) FUN_IN_IMAGE : !f s x. x IN s ==> f x IN IMAGE f s IMAGE_CONST : !s c. IMAGE (\x. c) s = (if s = {} then {} else {c}) IMAGE_DELETE_INJ : !f s a. (!x. f x = f a ==> x = a) ==> IMAGE f (s DELETE a) = IMAGE f s DELETE f a IMAGE_DIFF_INJ : !f s t. (!x y. f x = f y ==> x = y) ==> IMAGE f (s DIFF t) = IMAGE f s DIFF IMAGE f t IMAGE_EMPTY : !f. IMAGE f {} = {} IMAGE_EQ_EMPTY : !f s. IMAGE f s = {} <=> s = {} IMAGE_I : !s. IMAGE I s = s IMAGE_ID : !s. IMAGE (\x. x) s = s IMAGE_INJECTIVE_IMAGE_OF_SUBSET : !f s. ?t. t SUBSET s /\ IMAGE f s = IMAGE f t /\ (!x y. x IN t /\ y IN t /\ f x = f y ==> x = y) IMAGE_INSERT : !f x s. IMAGE f (x INSERT s) = f x INSERT IMAGE f s IMAGE_INTERS : !f s. ~(s = {}) /\ (!x y. x IN UNIONS s /\ y IN UNIONS s /\ f x = f y ==> x = y) ==> IMAGE f (INTERS s) = INTERS (IMAGE (IMAGE f) s) IMAGE_INTER_INJ : !f s t. (!x y. f x = f y ==> x = y) ==> IMAGE f (s INTER t) = IMAGE f s INTER IMAGE f t IMAGE_POWERSET : !s. {t | t SUBSET s} = IMAGE (\p. {x | p x}) {p | (!x. x IN s ==> p x IN UNIV) /\ (!x. ~(x IN s) ==> (p x <=> F))} IMAGE_SING : !f x. IMAGE f {x} = {f x} IMAGE_SUBSET : !f s t. s SUBSET t ==> IMAGE f s SUBSET IMAGE f t IMAGE_UNION : !f s t. IMAGE f (s UNION t) = IMAGE f s UNION IMAGE f t IMAGE_UNIONS : !f s. IMAGE f (UNIONS s) = UNIONS (IMAGE (IMAGE f) s) IMAGE_o : !f g s. IMAGE (f o g) s = IMAGE f (IMAGE g s) INJECTIVE_IMAGE : !f. (!s t. IMAGE f s = IMAGE f t ==> s = t) <=> (!x y. f x = f y ==> x = y) INJECTIVE_LEFT_INVERSE : !f. (!x y. f x = f y ==> x = y) <=> (?g. !x. g (f x) = x) INJECTIVE_ON_IMAGE : !f u. (!s t. s SUBSET u /\ t SUBSET u /\ IMAGE f s = IMAGE f t ==> s = t) <=> (!x y. x IN u /\ y IN u /\ f x = f y ==> x = y) INJECTIVE_ON_LEFT_INVERSE : !f s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) <=> (?g. !x. x IN s ==> g (f x) = x) INSERT_AC : !x y s. x INSERT y INSERT s = y INSERT x INSERT s /\ x INSERT x INSERT s = x INSERT s INSERT_BOOL : UNIV = {T, F} INSERT_COMM : !x y s. x INSERT y INSERT s = y INSERT x INSERT s INSERT_DELETE : !x s. x IN s ==> x INSERT (s DELETE x) = s INSERT_DIFF : !s t x. x INSERT s DIFF t = (if x IN t then s DIFF t else x INSERT (s DIFF t)) INSERT_FUNSPACE : !d a s t. {f | (!x. x IN a INSERT s ==> f x IN t) /\ (!x. ~(x IN a INSERT s) ==> f x = d)} = IMAGE (\(b,g) x. if x = a then b else g x) (t CROSS {f | (!x. x IN s ==> f x IN t) /\ (!x. ~(x IN s) ==> f x = d)}) INSERT_INSERT : !x s. x INSERT x INSERT s = x INSERT s INSERT_INTER : !x s t. x INSERT s INTER t = (if x IN t then x INSERT (s INTER t) else s INTER t) INSERT_NUMSEG_LT : !n. {m | m < SUC n} = n INSERT {m | m < n} INSERT_NUMSEG_LT' : !n. {m | m < SUC n} = 0 INSERT {SUC m | m < n} INSERT_POWERSET : !a t. {s | s SUBSET a INSERT t} = {s | s SUBSET t} UNION IMAGE (\s. a INSERT s) {s | s SUBSET t} INSERT_PRODUCT_DEPENDENT : !s t a. {x,y | x IN a INSERT s /\ y IN t x} = IMAGE ((,) a) (t a) UNION {x,y | x IN s /\ y IN t x} INSERT_SUBSET : !x s t. x INSERT s SUBSET t <=> x IN t /\ s SUBSET t INSERT_UNION : !x s t. x INSERT s UNION t = (if x IN t then s UNION t else x INSERT (s UNION t)) INSERT_UNION_EQ : !x s t. x INSERT s UNION t = x INSERT (s UNION t) INSERT_UNION_SING : !x s. {x} UNION s = x INSERT s INSERT_UNIV : !x. x INSERT UNIV = UNIV INTERS_0 : INTERS {} = UNIV INTERS_1 : !s. INTERS {s} = s INTERS_2 : !s t. INTERS {s, t} = s INTER t INTERS_GSPEC1 : !p f. INTERS {f x | p x} = {a | !x. p x ==> a IN f x} INTERS_GSPEC2 : !p f. INTERS {f x y | p x y} = {a | !x y. p x y ==> a IN f x y} INTERS_GSPEC3 : !p f. INTERS {f x y z | p x y z} = {a | !x y z. p x y z ==> a IN f x y z} INTERS_IMAGE : !f s. INTERS (IMAGE f s) = {y | !x. x IN s ==> y IN f x} INTERS_INSERT : !s u. INTERS (s INSERT u) = s INTER INTERS u INTERS_OVER_UNIONS : !f s. INTERS {UNIONS (f x) | x IN s} = UNIONS {INTERS {g x | x IN s} | g | !x. x IN s ==> g x IN f x} INTERS_SUBSET : !u s. ~(u = {}) /\ (!t. t IN u ==> t SUBSET s) ==> INTERS u SUBSET s INTERS_SUBSET_INTERS : !s t. s SUBSET t ==> INTERS t SUBSET INTERS s INTERS_UNION : !s t. INTERS (s UNION t) = INTERS s INTER INTERS t INTERS_UNIONS : !s. INTERS s = UNIV DIFF UNIONS {UNIV DIFF t | t IN s} INTER_ACI : !p q r. p INTER q = q INTER p /\ (p INTER q) INTER r = p INTER q INTER r /\ p INTER q INTER r = q INTER p INTER r /\ p INTER p = p /\ p INTER p INTER q = p INTER q INTER_ASSOC : !s t u. (s INTER t) INTER u = s INTER t INTER u INTER_COMM : !s t. s INTER t = t INTER s INTER_IDEMPOT : !s. s INTER s = s INTER_LEFT_EMPTY : !s. {} INTER s = {} INTER_LEFT_UNIV : !s. UNIV INTER s = s INTER_RIGHT_EMPTY : !s. s INTER {} = {} INTER_RIGHT_UNIV : !s. s INTER UNIV = s INTER_UNIONS : !s t. t INTER UNIONS s = UNIONS {t INTER x | x IN s} IN_CROSS : !x y s t. x,y IN s CROSS t <=> x IN s /\ y IN t IN_DELETE : !s x y. x IN s DELETE y <=> x IN s /\ ~(x = y) IN_DELETE_EQ : !s x x'. (x IN s DELETE x' <=> x' IN s DELETE x) <=> x IN s <=> x' IN s IN_DELETE_SWAP : !s x x'. (x IN s <=> x' IN s) ==> (x IN s DELETE x' <=> x' IN s DELETE x) IN_DIFF : !s t x. x IN s DIFF t <=> x IN s /\ ~(x IN t) IN_DISJOINT : !s t. DISJOINT s t <=> ~(?x. x IN s /\ x IN t) IN_ELIM : !p x. x IN {y | p y} <=> p x IN_ELIM_PAIR_THM : !p a b. a,b IN {x,y | p x y} <=> p a b IN_IMAGE : !y s f. y IN IMAGE f s <=> (?x. y = f x /\ x IN s) IN_INSERT : !x y s. x IN y INSERT s <=> x = y \/ x IN s IN_INTER : !s t x. x IN s INTER t <=> x IN s /\ x IN t IN_INTERS : !s x. x IN INTERS s <=> (!t. t IN s ==> x IN t) IN_REST : !x s. x IN REST s <=> x IN s /\ ~(x = CHOICE s) IN_SING : !x y. x IN {y} <=> x = y IN_UNION : !s t x. x IN s UNION t <=> x IN s \/ x IN t IN_UNIONS : !s x. x IN UNIONS s <=> (?t. t IN s /\ x IN t) IN_UNIV : !x. x IN UNIV LEFT_INTER_DISTRIB : !s t u. s UNION t INTER u = (s UNION t) INTER (s UNION u) LEFT_INTER_SUBSET : !s t. s INTER t SUBSET s LEFT_UNION_DISTRIB : !s t u. s INTER (t UNION u) = s INTER t UNION s INTER u LEFT_UNION_INTERS : !s t. t UNION INTERS s = INTERS {t UNION x | x IN s} MEMBER_NOT_EMPTY : !s. (?x. x IN s) <=> ~(s = {}) NOT_EQUAL_SETS : !s t. ~(s = t) <=> (?x. x IN t <=> ~(x IN s)) NOT_INSERT_EMPTY : !x s. ~(x INSERT s = {}) NOT_IN_EMPTY : !x. ~(x IN {}) NOT_PSUBSET_EMPTY : !s. ~(s PSUBSET {}) NOT_UNIV_PSUBSET : !s. ~(UNIV PSUBSET s) PSUBSET_ALT : !s t. s PSUBSET t <=> s SUBSET t /\ (?a. a IN t /\ ~(a IN s)) PSUBSET_INSERT_SUBSET : !s t. s PSUBSET t <=> (?x. ~(x IN s) /\ x INSERT s SUBSET t) PSUBSET_IRREFL : !s. ~(s PSUBSET s) PSUBSET_NOT_SUBSET : !s t. s PSUBSET t <=> s SUBSET t /\ ~(t SUBSET s) PSUBSET_SUBSET : !s t. s PSUBSET t ==> s SUBSET t PSUBSET_SUBSET_TRANS : !s t u. s PSUBSET t /\ t SUBSET u ==> s PSUBSET u PSUBSET_TRANS : !s t u. s PSUBSET t /\ t PSUBSET u ==> s PSUBSET u PSUBSET_UNIV : !s. s PSUBSET UNIV <=> (?x. ~(x IN s)) RIGHT_INTER_DISTRIB : !s t u. s INTER t UNION u = (s UNION u) INTER (t UNION u) RIGHT_INTER_SUBSET : !s t. t INTER s SUBSET s RIGHT_UNION_DISTRIB : !s t u. (s UNION t) INTER u = s INTER u UNION t INTER u RIGHT_UNION_INTERS : !s t. INTERS s UNION t = INTERS {x UNION t | x IN s} SET_CASES : !s. s = {} \/ (?x t. s = x INSERT t /\ ~(x IN t)) SET_PAIR_THM : !p. {x | p x} = {a,b | p (a,b)} SET_PROVE_CASES : !p. p {} /\ (!a s. ~(a IN s) ==> p (a INSERT s)) ==> (!s. p s) SIMPLE_IMAGE : !f s. {f x | x IN s} = IMAGE f s SIMPLE_IMAGE_GEN : !p f. {f x | p x} = IMAGE f {x | p x} SING_DISJOINT : !x s. DISJOINT {x} s <=> ~(x IN s) SING_GSPEC1 : !a. {x | x = a} = {a} SING_SUBSET : !s x. {x} SUBSET s <=> x IN s SUBSET_ANTISYM : !s t. s SUBSET t /\ t SUBSET s ==> s = t SUBSET_ANTISYM_EQ : !s t. s SUBSET t /\ t SUBSET s <=> s = t SUBSET_DELETE : !x s t. s SUBSET t DELETE x <=> s SUBSET t /\ ~(x IN s) SUBSET_DIFF : !s t u. s SUBSET t DIFF u <=> s SUBSET t /\ DISJOINT s u SUBSET_DIFF_UNION : !s t u. s SUBSET t UNION u <=> s DIFF t SUBSET u SUBSET_EMPTY : !s. s SUBSET {} <=> s = {} SUBSET_IMAGE : !f s t. s SUBSET IMAGE f t <=> (?u. u SUBSET t /\ s = IMAGE f u) SUBSET_IMAGE_INJ : !f s t. s SUBSET IMAGE f t <=> (?u. u SUBSET t /\ (!x y. x IN u /\ y IN u /\ f x = f y ==> x = y) /\ s = IMAGE f u) SUBSET_INSERT : !x s. ~(x IN s) ==> (!t. s SUBSET x INSERT t <=> s SUBSET t) SUBSET_INSERT_DELETE : !x s t. s SUBSET x INSERT t <=> s DELETE x SUBSET t SUBSET_INSERT_IMP : !s t x. s SUBSET t ==> s SUBSET x INSERT t SUBSET_INTER : !s t u. s SUBSET t INTER u <=> s SUBSET t /\ s SUBSET u SUBSET_INTERS : !t u. t SUBSET INTERS u <=> (!s. s IN u ==> t SUBSET s) SUBSET_INTER_ABSORPTION : !s t. s SUBSET t <=> s INTER t = s SUBSET_LEFT_UNION : !s t. s SUBSET s UNION t SUBSET_PSUBSET_TRANS : !s t u. s SUBSET t /\ t PSUBSET u ==> s PSUBSET u SUBSET_REFL : !s. s SUBSET s SUBSET_RESTRICT : !s p. {x | x IN s /\ p x} SUBSET s SUBSET_RIGHT_UNION : !s t. s SUBSET t UNION s SUBSET_SING : !s x. s SUBSET {x} <=> s = {} \/ s = {x} SUBSET_TRANS : !s t u. s SUBSET t /\ t SUBSET u ==> s SUBSET u SUBSET_UNIONS : !f g. f SUBSET g ==> UNIONS f SUBSET UNIONS g SUBSET_UNION_ABSORPTION : !s t. s SUBSET t <=> s UNION t = t SUBSET_UNION_DIFF : !s t u. s SUBSET t UNION u <=> s DIFF u SUBSET t SUBSET_UNIV : !s. s SUBSET UNIV SURJECTIVE_IMAGE : !f. (!t. ?s. IMAGE f s = t) <=> (!y. ?x. f x = y) SURJECTIVE_IMAGE_EQ : !f s t. (!y. y IN t ==> (?x. f x = y)) /\ (!x. f x IN t <=> x IN s) ==> IMAGE f s = t SURJECTIVE_IMAGE_THM : !f. (!y. ?x. f x = y) <=> (!p. IMAGE f {x | p (f x)} = {x | p x}) SURJECTIVE_ON_IMAGE : !f u v. (!t. t SUBSET v ==> (?s. s SUBSET u /\ IMAGE f s = t)) <=> (!y. y IN v ==> (?x. x IN u /\ f x = y)) SURJECTIVE_ON_RIGHT_INVERSE : !f s t. (!y. y IN t ==> (?x. x IN s /\ f x = y)) <=> (?g. !y. y IN t ==> g y IN s /\ f (g y) = y) SURJECTIVE_RIGHT_INVERSE : !f. (!y. ?x. f x = y) <=> (?g. !y. f (g y) = y) UNIONS_0 : UNIONS {} = {} UNIONS_1 : !s. UNIONS {s} = s UNIONS_2 : !s t. UNIONS {s, t} = s UNION t UNIONS_DIFF : !s t. UNIONS s DIFF t = UNIONS {x DIFF t | x IN s} UNIONS_GSPEC1 : !p f. UNIONS {f x | p x} = {a | ?x. p x /\ a IN f x} UNIONS_GSPEC2 : !p f. UNIONS {f x y | p x y} = {a | ?x y. p x y /\ a IN f x y} UNIONS_GSPEC3 : !p f. UNIONS {f x y z | p x y z} = {a | ?x y z. p x y z /\ a IN f x y z} UNIONS_IMAGE : !f s. UNIONS (IMAGE f s) = {y | ?x. x IN s /\ y IN f x} UNIONS_INSERT : !s u. UNIONS (s INSERT u) = s UNION UNIONS u UNIONS_INTER : !s t. UNIONS s INTER t = UNIONS {x INTER t | x IN s} UNIONS_INTERS : !s. UNIONS s = UNIV DIFF INTERS {UNIV DIFF t | t IN s} UNIONS_MONO : !s t. (!x. x IN s ==> (?y. y IN t /\ x SUBSET y)) ==> UNIONS s SUBSET UNIONS t UNIONS_OVER_INTERS : !f s. UNIONS {INTERS (f x) | x IN s} = INTERS {UNIONS {g x | x IN s} | g | !x. x IN s ==> g x IN f x} UNIONS_SUBSET : !f t. UNIONS f SUBSET t <=> (!s. s IN f ==> s SUBSET t) UNIONS_UNION : !s t. UNIONS (s UNION t) = UNIONS s UNION UNIONS t UNION_ACI : !p q r. p UNION q = q UNION p /\ (p UNION q) UNION r = p UNION q UNION r /\ p UNION q UNION r = q UNION p UNION r /\ p UNION p = p /\ p UNION p UNION q = p UNION q UNION_ASSOC : !s t u. (s UNION t) UNION u = s UNION t UNION u UNION_COMM : !s t. s UNION t = t UNION s UNION_DIFF_CANCEL : !s t. t UNION s DIFF t = t UNION s UNION_DIFF_SUBSET : !s t. s UNION t DIFF s = t <=> s SUBSET t UNION_IDEMPOT : !s. s UNION s = s UNION_LEFT_EMPTY : !s. {} UNION s = s UNION_LEFT_UNIV : !s. UNIV UNION s = UNIV UNION_RIGHT_EMPTY : !s. s UNION {} = s UNION_RIGHT_UNIV : !s. s UNION UNIV = UNIV UNION_SUBSET : !s t u. s UNION t SUBSET u <=> s SUBSET u /\ t SUBSET u UNIV_GSPEC : GSPEC (\x. T) = UNIV UNIV_INTERS : !s. INTERS s = UNIV <=> (!t. t IN s ==> t = UNIV) UNIV_NOT_EMPTY : ~(UNIV = {}) UNIV_SUBSET : !s. UNIV SUBSET s <=> s = UNIV

Back to main package page