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