Entry Value
Package Name set-size-thm
Count 68
Theorems
  • BIJECTIONS_CARD_EQ : !s t f g. (FINITE s \/ FINITE t) /\ (!x. x IN s ==> f x IN t /\ g (f x) = x) /\ (!y. y IN t ==> g y IN s /\ f (g y) = y) ==> CARD s = CARD t
  • BIJECTIONS_HAS_SIZE : !s t f g n. (!x. x IN s ==> f x IN t /\ g (f x) = x) /\ (!y. y IN t ==> g y IN s /\ f (g y) = y) /\ s HAS_SIZE n ==> t HAS_SIZE n
  • BIJECTIONS_HAS_SIZE_EQ : !s t f g. (!x. x IN s ==> f x IN t /\ g (f x) = x) /\ (!y. y IN t ==> g y IN s /\ f (g y) = y) ==> (!n. s HAS_SIZE n <=> t HAS_SIZE n)
  • CARD_CROSS : !s t. FINITE s /\ FINITE t ==> CARD (s CROSS t) = CARD s * CARD t
  • CARD_DELETE : !x s. FINITE s ==> CARD (s DELETE x) = (if x IN s then CARD s - 1 else CARD s)
  • CARD_DIFF : !s t. FINITE s /\ t SUBSET s ==> CARD (s DIFF t) = CARD s - CARD t
  • CARD_EMPTY : CARD {} = 0
  • CARD_EQ_0 : !s. FINITE s ==> (CARD s = 0 <=> s = {})
  • CARD_EQ_BIJECTION : !s t. FINITE s /\ FINITE t /\ CARD s = CARD t ==> (?f. (!x. x IN s ==> f x IN t) /\ (!y. y IN t ==> (?x. x IN s /\ f x = y)) /\ (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y))
  • CARD_EQ_BIJECTIONS : !s t. FINITE s /\ FINITE t /\ CARD s = CARD t ==> (?f g. (!x. x IN s ==> f x IN t /\ g (f x) = x) /\ (!y. y IN t ==> g y IN s /\ f (g y) = y))
  • CARD_FUNSPACE : !d s t. FINITE s /\ FINITE t ==> CARD {f | (!x. x IN s ==> f x IN t) /\ (!x. ~(x IN s) ==> f x = d)} = CARD t EXP CARD s
  • CARD_FUNSPACE_UNIV : FINITE UNIV /\ FINITE UNIV ==> CARD UNIV = CARD UNIV EXP CARD UNIV
  • CARD_IMAGE_EQ_INJ : !f s. FINITE s ==> (CARD (IMAGE f s) = CARD s <=> (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y))
  • CARD_IMAGE_INJ : !f s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\ FINITE s ==> CARD (IMAGE f s) = CARD s
  • CARD_IMAGE_INJ_EQ : !f s t. FINITE s /\ (!x. x IN s ==> f x IN t) /\ (!y. y IN t ==> (?!x. x IN s /\ f x = y)) ==> CARD t = CARD s
  • CARD_IMAGE_LE : !f s. FINITE s ==> CARD (IMAGE f s) <= CARD s
  • CARD_INSERT : !x s. FINITE s ==> CARD (x INSERT s) = (if x IN s then CARD s else SUC (CARD s))
  • CARD_LE_INJ : !s t. FINITE s /\ FINITE t /\ CARD s <= CARD t ==> (?f. IMAGE f s SUBSET t /\ (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y))
  • CARD_NUMSEG_LE : !n. CARD {m | m <= n} = n + 1
  • CARD_NUMSEG_LT : !n. CARD {m | m < n} = n
  • CARD_POWERSET : !s. FINITE s ==> CARD {t | t SUBSET s} = 2 EXP CARD s
  • CARD_PRODUCT : !s t. FINITE s /\ FINITE t ==> CARD {x,y | x IN s /\ y IN t} = CARD s * CARD t
  • CARD_PSUBSET : !a b. a PSUBSET b /\ FINITE b ==> CARD a < CARD b
  • CARD_SING : !x. CARD {x} = 1
  • CARD_SUBSET : !a b. a SUBSET b /\ FINITE b ==> CARD a <= CARD b
  • CARD_SUBSET_EQ : !a b. FINITE b /\ a SUBSET b /\ CARD a = CARD b ==> a = b
  • CARD_SUBSET_IMAGE : !f s t. FINITE t /\ s SUBSET IMAGE f t ==> CARD s <= CARD t
  • CARD_SUBSET_LE : !a b. FINITE b /\ a SUBSET b /\ CARD b <= CARD a ==> a = b
  • CARD_UNION : !s t. FINITE s /\ FINITE t /\ DISJOINT s t ==> CARD (s UNION t) = CARD s + CARD t
  • CARD_UNIONS_LE : !s t m n. s HAS_SIZE m /\ (!x. x IN s ==> FINITE (t x) /\ CARD (t x) <= n) ==> CARD (UNIONS {t x | x IN s}) <= m * n
  • CARD_UNION_DIFF : !s t. FINITE s /\ FINITE t ==> CARD (s UNION t) = CARD s + CARD (t DIFF s)
  • CARD_UNION_EQ : !s t u. FINITE u /\ DISJOINT s t /\ s UNION t = u ==> CARD s + CARD t = CARD u
  • CARD_UNION_GEN : !s t. FINITE s /\ FINITE t ==> CARD (s UNION t) = (CARD s + CARD t) - CARD (s INTER t)
  • CARD_UNION_INTER : !s t. FINITE s /\ FINITE t ==> CARD (s UNION t) + CARD (s INTER t) = CARD s + CARD t
  • CARD_UNION_LE : !s t. FINITE s /\ FINITE t ==> CARD (s UNION t) <= CARD s + CARD t
  • CARD_UNION_OVERLAP : !s t. FINITE s /\ FINITE t /\ CARD (s UNION t) < CARD s + CARD t ==> ~DISJOINT s t
  • CARD_UNION_OVERLAP_EQ : !s t. FINITE s /\ FINITE t ==> (CARD (s UNION t) = CARD s + CARD t <=> DISJOINT s t)
  • CHOOSE_SUBSET : !s n. FINITE s /\ n <= CARD s ==> (?t. t SUBSET s /\ t HAS_SIZE n)
  • CHOOSE_SUBSET_BETWEEN : !n s u. s SUBSET u /\ FINITE s /\ CARD s <= n /\ (FINITE u ==> n <= CARD u) ==> (?t. s SUBSET t /\ t SUBSET u /\ t HAS_SIZE n)
  • CHOOSE_SUBSET_STRONG : !s n. (FINITE s ==> n <= CARD s) ==> (?t. t SUBSET s /\ t HAS_SIZE n)
  • FINITE_FUNSPACE_UNIV : FINITE UNIV /\ FINITE UNIV ==> FINITE UNIV
  • FINITE_HAS_SIZE : !s. FINITE s <=> s HAS_SIZE CARD s
  • FINITE_INDUCT_DELETE : !p. p {} /\ (!s. FINITE s /\ ~(s = {}) ==> (?x. x IN s /\ (p (s DELETE x) ==> p s))) ==> (!s. FINITE s ==> p s)
  • HAS_SIZE_0 : !s. s HAS_SIZE 0 <=> s = {}
  • HAS_SIZE_BOOL : UNIV HAS_SIZE 2
  • HAS_SIZE_CARD : !s n. s HAS_SIZE n ==> CARD s = n
  • HAS_SIZE_CROSS : !s t m n. s HAS_SIZE m /\ t HAS_SIZE n ==> s CROSS t HAS_SIZE m * n
  • HAS_SIZE_DIFF : !s t m n. s HAS_SIZE m /\ t HAS_SIZE n /\ t SUBSET s ==> s DIFF t HAS_SIZE m - n
  • HAS_SIZE_FUNSPACE : !d s t m n. s HAS_SIZE m /\ t HAS_SIZE n ==> {f | (!x. x IN s ==> f x IN t) /\ (!x. ~(x IN s) ==> f x = d)} HAS_SIZE n EXP m
  • HAS_SIZE_FUNSPACE_UNIV : !m n. UNIV HAS_SIZE m /\ UNIV HAS_SIZE n ==> UNIV HAS_SIZE n EXP m
  • HAS_SIZE_IMAGE_INJ : !f s n. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\ s HAS_SIZE n ==> IMAGE f s HAS_SIZE n
  • HAS_SIZE_IMAGE_INJ_EQ : !f s n. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) ==> (IMAGE f s HAS_SIZE n <=> s HAS_SIZE n)
  • HAS_SIZE_INDEX : !s n. s HAS_SIZE n ==> (?f. (!m. m < n ==> f m IN s) /\ (!x. x IN s ==> (?!m. m < n /\ f m = x)))
  • HAS_SIZE_INSERT : !s n. s HAS_SIZE SUC n <=> (?a t. t HAS_SIZE n /\ ~(a IN t) /\ s = a INSERT t)
  • HAS_SIZE_NUMSEG_LE : !n. {m | m <= n} HAS_SIZE n + 1
  • HAS_SIZE_NUMSEG_LT : !n. {m | m < n} HAS_SIZE n
  • HAS_SIZE_POWERSET : !s n. s HAS_SIZE n ==> {t | t SUBSET s} HAS_SIZE 2 EXP n
  • HAS_SIZE_PRODUCT : !s t m n. s HAS_SIZE m /\ t HAS_SIZE n ==> {x,y | x IN s /\ y IN t} HAS_SIZE m * n
  • HAS_SIZE_PRODUCT_DEPENDENT : !s t m n. s HAS_SIZE m /\ (!x. x IN s ==> t x HAS_SIZE n) ==> {x,y | x IN s /\ y IN t x} HAS_SIZE m * n
  • HAS_SIZE_SING : !x. {x} HAS_SIZE 1
  • HAS_SIZE_SUC : !s n. s HAS_SIZE SUC n <=> ~(s = {}) /\ (!a. a IN s ==> s DELETE a HAS_SIZE n)
  • HAS_SIZE_UNION : !s t m n. s HAS_SIZE m /\ t HAS_SIZE n /\ DISJOINT s t ==> s UNION t HAS_SIZE m + n
  • HAS_SIZE_UNIONS : !s t m n. s HAS_SIZE m /\ (!x. x IN s ==> t x HAS_SIZE n) /\ (!x y. x IN s /\ y IN s /\ ~(x = y) ==> DISJOINT (t x) (t y)) ==> UNIONS {t x | x IN s} HAS_SIZE m * n
  • IMAGE_IMP_INJECTIVE : !s f. FINITE s /\ IMAGE f s = s ==> (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)
  • IMAGE_IMP_INJECTIVE_GEN : !s t f. FINITE s /\ CARD s = CARD t /\ IMAGE f s = t ==> (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)
  • SUBSET_CARD_EQ : !s t. FINITE t /\ s SUBSET t ==> (CARD s = CARD t <=> s = t)
  • SURJECTIVE_IFF_INJECTIVE : !s f. FINITE s /\ IMAGE f s SUBSET s ==> ((!y. y IN s ==> (?x. x IN s /\ f x = y)) <=> (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y))
  • SURJECTIVE_IFF_INJECTIVE_GEN : !s t f. FINITE s /\ FINITE t /\ CARD s = CARD t /\ IMAGE f s SUBSET t ==> ((!y. y IN t ==> (?x. x IN s /\ f x = y)) <=> (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y))
    		•
    Back to main package page