Entry	Value
Package Name	set-finite-thm
Count	46
Theorems	EXISTS_FINITE_SUBSET_IMAGE : !p f s. (?t. FINITE t /\ t SUBSET IMAGE f s /\ p t) <=> (?t. FINITE t /\ t SUBSET s /\ p (IMAGE f t)) EXISTS_FINITE_SUBSET_IMAGE_INJ : !p f s. (?t. FINITE t /\ t SUBSET IMAGE f s /\ p t) <=> (?t. FINITE t /\ t SUBSET s /\ (!x y. x IN t /\ y IN t /\ f x = f y ==> x = y) /\ p (IMAGE f t)) FINITE_BOOL : FINITE UNIV FINITE_CROSS : !s t. FINITE s /\ FINITE t ==> FINITE (s CROSS t) FINITE_CROSS_EQ : !s t. FINITE (s CROSS t) <=> s = {} \/ t = {} \/ FINITE s /\ FINITE t FINITE_DELETE : !s x. FINITE (s DELETE x) <=> FINITE s FINITE_DELETE_IMP : !s x. FINITE s ==> FINITE (s DELETE x) FINITE_DIFF : !s t. FINITE s ==> FINITE (s DIFF t) FINITE_FINITE_PREIMAGE : !f t. FINITE t /\ (!y. y IN t ==> FINITE {x | f x = y}) ==> FINITE {x | f x IN t} FINITE_FINITE_PREIMAGE_GENERAL : !f s t. FINITE t /\ (!y. y IN t ==> FINITE {x | x IN s /\ f x = y}) ==> FINITE {x | x IN s /\ f x IN t} FINITE_FINITE_UNIONS : !s. FINITE s ==> (FINITE (UNIONS s) <=> (!t. t IN s ==> FINITE t)) FINITE_FUNSPACE : !d s t. FINITE s /\ FINITE t ==> FINITE {f | (!x. x IN s ==> f x IN t) /\ (!x. ~(x IN s) ==> f x = d)} FINITE_IMAGE : !f s. FINITE s ==> FINITE (IMAGE f s) FINITE_IMAGE_EXPAND : !f s. FINITE s ==> FINITE {y | ?x. x IN s /\ y = f x} FINITE_IMAGE_INJ : !f A. (!x y. f x = f y ==> x = y) /\ FINITE A ==> FINITE {x | f x IN A} FINITE_IMAGE_INJ_EQ : !f s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) ==> (FINITE (IMAGE f s) <=> FINITE s) FINITE_IMAGE_INJ_GENERAL : !f t s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\ FINITE t ==> FINITE {x | x IN s /\ f x IN t} FINITE_INDUCT_STRONG : !p. p {} /\ (!x s. p s /\ ~(x IN s) /\ FINITE s ==> p (x INSERT s)) ==> (!s. FINITE s ==> p s) FINITE_INSERT : !s x. FINITE (x INSERT s) <=> FINITE s FINITE_INTER : !s t. FINITE s \/ FINITE t ==> FINITE (s INTER t) FINITE_NUMSEG_LE : !n. FINITE {m | m <= n} FINITE_NUMSEG_LT : !n. FINITE {m | m < n} FINITE_POWERSET : !s. FINITE s ==> FINITE {t | t SUBSET s} FINITE_PRODUCT : !s t. FINITE s /\ FINITE t ==> FINITE {x,y | x IN s /\ y IN t} FINITE_PRODUCT_DEPENDENT : !f s t. FINITE s /\ (!x. x IN s ==> FINITE (t x)) ==> FINITE {f x y | x IN s /\ y IN t x} FINITE_RESTRICT : !s p. FINITE s ==> FINITE {x | x IN s /\ p x} FINITE_SING : !a. FINITE {a} FINITE_SUBSET : !s t. FINITE t /\ s SUBSET t ==> FINITE s FINITE_SUBSET_IMAGE : !f s t. FINITE t /\ t SUBSET IMAGE f s <=> (?s'. FINITE s' /\ s' SUBSET s /\ t = IMAGE f s') FINITE_SUBSET_IMAGE_IMP : !f s t. FINITE t /\ t SUBSET IMAGE f s ==> (?s'. FINITE s' /\ s' SUBSET s /\ t SUBSET IMAGE f s') FINITE_TRANSITIVITY_CHAIN : !r s. FINITE s /\ (!x. ~r x x) /\ (!x y z. r x y /\ r y z ==> r x z) /\ (!x. x IN s ==> (?y. y IN s /\ r x y)) ==> s = {} FINITE_UNION : !s t. FINITE (s UNION t) <=> FINITE s /\ FINITE t FINITE_UNIONS : !s. FINITE (UNIONS s) <=> FINITE s /\ (!t. t IN s ==> FINITE t) FINITE_UNION_IMP : !s t. FINITE s /\ FINITE t ==> FINITE (s UNION t) FORALL_FINITE_SUBSET_IMAGE : !p f s. (!t. FINITE t /\ t SUBSET IMAGE f s ==> p t) <=> (!t. FINITE t /\ t SUBSET s ==> p (IMAGE f t)) FORALL_FINITE_SUBSET_IMAGE_INJ : !p f s. (!t. FINITE t /\ t SUBSET IMAGE f s ==> p t) <=> (!t. FINITE t /\ t SUBSET s /\ (!x y. x IN t /\ y IN t /\ f x = f y ==> x = y) ==> p (IMAGE f t)) INFINITE_DIFF_FINITE : !s t. INFINITE s /\ FINITE t ==> INFINITE (s DIFF t) INFINITE_ENUMERATE : !s. INFINITE s ==> (?r. (!m n. m < n ==> r m < r n) /\ IMAGE r UNIV = s) INFINITE_IMAGE_INJ : !f s. INFINITE s /\ (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) ==> INFINITE (IMAGE f s) INFINITE_IMAGE_INJ_EQ : !f. (!x y. f x = f y ==> x = y) ==> (!s. INFINITE (IMAGE f s) <=> INFINITE s) INFINITE_NONEMPTY : !s. INFINITE s ==> ~(s = {}) INFINITE_SUPERSET : !s t. INFINITE s /\ s SUBSET t ==> INFINITE t UNIONS_MAXIMAL_SETS : !f. FINITE f ==> UNIONS {t | t IN f /\ (!u. u IN f ==> ~(t PSUBSET u))} = UNIONS f num_FINITE : !s. FINITE s <=> (?a. !x. x IN s ==> x <= a) num_FINITE_AVOID : !s. FINITE s ==> (?a. ~(a IN s)) num_INFINITE : INFINITE UNIV

Back to main package page