Entry	Value
Package Name	set-def
Count	22
Theorems	BIJ : !s t. BIJ s t = INJ s t INTER SURJ s t CHOICE : !s. ~(s = {}) ==> CHOICE s IN s CROSS : !s t. s CROSS t = {x,y | x IN s /\ y IN t} DELETE : !s x. s DELETE x = {y | y IN s /\ ~(y = x)} DIFF : !s t. s DIFF t = {x | x IN s /\ ~(x IN t)} DISJOINT : !s t. DISJOINT s t <=> s INTER t = {} EMPTY : {} = {x | F} EXTENSION_IMP : !s t. (!x. x IN s <=> x IN t) ==> s = t IMAGE : !f s. IMAGE f s = {y | ?x. x IN s /\ y = f x} INJ : !s t. INJ s t = {f | (!x. x IN s ==> f x IN t) /\ (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)} INSERT : !x s. x INSERT s = {y | y = x \/ y IN s} INTER : !s t. s INTER t = {x | x IN s /\ x IN t} INTERS : !s. INTERS s = {x | !u. u IN s ==> x IN u} IN_ELIM_THM : !p x. x IN GSPEC p <=> p x PSUBSET : !s t. s PSUBSET t <=> s SUBSET t /\ ~(s = t) REST : !s. REST s = s DELETE CHOICE s SING : !s. SING s <=> (?x. s = {x}) SUBSET : !s t. s SUBSET t <=> (!x. x IN s ==> x IN t) SURJ : !s t. SURJ s t = {f | (!x. x IN s ==> f x IN t) /\ (!x. x IN t ==> (?y. y IN s /\ f y = x))} UNION : !s t. s UNION t = {x | x IN s \/ x IN t} UNIONS : !s. UNIONS s = {x | ?u. u IN s /\ x IN u} UNIV : UNIV = {x | T}

Back to main package page