Structure pred_setTheory
signature pred_setTheory =
sig
type thm = Thm.thm
(* Definitions *)
val BIGINTER : thm
val BIGUNION : thm
val BIJ_DEF : thm
val CARD_DEF : thm
val CHOICE_DEF : thm
val COMPL_DEF : thm
val CROSS_DEF : thm
val DELETE_DEF : thm
val DFUNSET : thm
val DIFF_DEF : thm
val DISJOINT_DEF : thm
val EMPTY_DEF : thm
val FINITE_DEF : thm
val FUNSET : thm
val GSPECIFICATION : thm
val HAS_SIZE : thm
val IMAGE_DEF : thm
val INJ_DEF : thm
val INSERT_DEF : thm
val INTER_DEF : thm
val LINV_LO : thm
val LINV_OPT_def : thm
val MAX_SET_DEF : thm
val MIN_SET_DEF : thm
val POW_DEF : thm
val PREIMAGE_def : thm
val PROD_IMAGE_DEF : thm
val PROD_SET_DEF : thm
val PSUBSET_DEF : thm
val REL_RESTRICT_DEF : thm
val REST_DEF : thm
val RINV_LO : thm
val SING_DEF : thm
val SUBSET_DEF : thm
val SUM_IMAGE_DEF : thm
val SUM_SET_DEF : thm
val SURJ_DEF : thm
val UNION_DEF : thm
val UNIV_DEF : thm
val chooser_def : thm
val closure_comm_assoc_fun_def : thm
val count_def : thm
val countable_def : thm
val disjUNION_def : thm
val disjoint : thm
val enumerate_def : thm
val equiv_on_def : thm
val is_measure_maximal_def : thm
val num_to_pair_def : thm
val pair_to_num_def : thm
val pairwise_def : thm
val part_def : thm
val partition_def : thm
val partitions_def : thm
val refines_def : thm
val schroeder_close_def : thm
(* Theorems *)
val ABSORPTION : thm
val ABSORPTION_RWT : thm
val ABS_DIFF_SUM_IMAGE : thm
val BIGINTER_2 : thm
val BIGINTER_EMPTY : thm
val BIGINTER_GSPEC : thm
val BIGINTER_IMAGE : thm
val BIGINTER_INSERT : thm
val BIGINTER_INTER : thm
val BIGINTER_SING : thm
val BIGINTER_SUBSET : thm
val BIGINTER_UNION : thm
val BIGINTER_applied : thm
val BIGUNION_CROSS : thm
val BIGUNION_EMPTY : thm
val BIGUNION_EQ_EMPTY : thm
val BIGUNION_GSPEC : thm
val BIGUNION_IMAGE : thm
val BIGUNION_IMAGE_SUBSET : thm
val BIGUNION_IMAGE_UNIV : thm
val BIGUNION_INSERT : thm
val BIGUNION_PAIR : thm
val BIGUNION_SING : thm
val BIGUNION_SUBSET : thm
val BIGUNION_UNION : thm
val BIGUNION_applied : thm
val BIGUNION_partition : thm
val BIJ_ALT : thm
val BIJ_COMPOSE : thm
val BIJ_CONG : thm
val BIJ_DELETE : thm
val BIJ_ELEMENT : thm
val BIJ_EMPTY : thm
val BIJ_FINITE : thm
val BIJ_FINITE_IFF : thm
val BIJ_FINITE_SUBSET : thm
val BIJ_ID : thm
val BIJ_IFF_INV : thm
val BIJ_IMAGE : thm
val BIJ_IMAGE_partitions : thm
val BIJ_IMP_11 : thm
val BIJ_INJ_SURJ : thm
val BIJ_INSERT : thm
val BIJ_INSERT_IMP : thm
val BIJ_INV : thm
val BIJ_IS_INJ : thm
val BIJ_IS_SURJ : thm
val BIJ_I_SAME : thm
val BIJ_LINV_BIJ : thm
val BIJ_LINV_INV : thm
val BIJ_NUM_COUNTABLE : thm
val BIJ_NUM_TO_PAIR : thm
val BIJ_PAIR_TO_NUM : thm
val BIJ_SWAP : thm
val BIJ_SYM : thm
val BIJ_SYM_IMP : thm
val BIJ_THM : thm
val BIJ_TRANS : thm
val BIJ_support : thm
val CARD_AS_SIGMA : thm
val CARD_BIGUNION_SAME_SIZED_SETS : thm
val CARD_CLAUSES : thm
val CARD_COUNT : thm
val CARD_CROSS : thm
val CARD_DELETE : thm
val CARD_DIFF : thm
val CARD_DIFF_EQN : thm
val CARD_EMPTY : thm
val CARD_EQ_0 : thm
val CARD_EQ_SIGMA : thm
val CARD_IMAGE : thm
val CARD_IMAGE_INJ : thm
val CARD_IMAGE_LE : thm
val CARD_IMAGE_SUC : thm
val CARD_INJ_IMAGE : thm
val CARD_INSERT : thm
val CARD_INTER_LESS_EQ : thm
val CARD_LE_MAX_SET : thm
val CARD_POW : thm
val CARD_PRODUCT : thm
val CARD_PSUBSET : thm
val CARD_REST : thm
val CARD_SING : thm
val CARD_SING_CROSS : thm
val CARD_SUBSET : thm
val CARD_UNION : thm
val CARD_UNION_DISJOINT : thm
val CARD_UNION_EQN : thm
val CARD_UNION_LE : thm
val CARD_disjUNION : thm
val CHOICE_INSERT_REST : thm
val CHOICE_INTRO : thm
val CHOICE_NOT_IN_REST : thm
val CHOICE_SING : thm
val COMMUTING_ITSET_INSERT : thm
val COMMUTING_ITSET_RECURSES : thm
val COMPL_CLAUSES : thm
val COMPL_COMPL : thm
val COMPL_EMPTY : thm
val COMPL_INTER : thm
val COMPL_SPLITS : thm
val COMPL_UNION : thm
val COMPL_applied : thm
val COMPONENT : thm
val COUNTABLE_ALT : thm
val COUNTABLE_ALT_BIJ : thm
val COUNTABLE_COUNT : thm
val COUNTABLE_ENUM : thm
val COUNTABLE_IMAGE_NUM : thm
val COUNTABLE_NUM : thm
val COUNTABLE_SUBSET : thm
val COUNT_11 : thm
val COUNT_DELETE : thm
val COUNT_EQ_EMPTY : thm
val COUNT_MONO : thm
val COUNT_NOT_EMPTY : thm
val COUNT_ONE : thm
val COUNT_SUC : thm
val COUNT_ZERO : thm
val COUNT_applied : thm
val CROSS_BIGUNION : thm
val CROSS_EMPTY : thm
val CROSS_EMPTY_EQN : thm
val CROSS_EQNS : thm
val CROSS_INSERT_LEFT : thm
val CROSS_INSERT_RIGHT : thm
val CROSS_SINGS : thm
val CROSS_SUBSET : thm
val CROSS_UNIV : thm
val CROSS_applied : thm
val DECOMPOSITION : thm
val DELETE_COMM : thm
val DELETE_DELETE : thm
val DELETE_EQ_SING : thm
val DELETE_INSERT : thm
val DELETE_INTER : thm
val DELETE_NON_ELEMENT : thm
val DELETE_NON_ELEMENT_RWT : thm
val DELETE_SUBSET : thm
val DELETE_SUBSET_INSERT : thm
val DELETE_applied : thm
val DFUNSET_applied : thm
val DIFF_BIGINTER : thm
val DIFF_BIGINTER1 : thm
val DIFF_COMM : thm
val DIFF_DIFF : thm
val DIFF_DIFF_SUBSET : thm
val DIFF_EMPTY : thm
val DIFF_EQ_EMPTY : thm
val DIFF_INSERT : thm
val DIFF_INTER : thm
val DIFF_INTER2 : thm
val DIFF_INTER_COMPL : thm
val DIFF_INTER_SUBSET : thm
val DIFF_SAME_UNION : thm
val DIFF_SUBSET : thm
val DIFF_UNION : thm
val DIFF_UNIV : thm
val DIFF_applied : thm
val DISJOINT_ALT : thm
val DISJOINT_ALT' : thm
val DISJOINT_BIGINTER : thm
val DISJOINT_BIGUNION : thm
val DISJOINT_COUNT : thm
val DISJOINT_DELETE_SYM : thm
val DISJOINT_DIFF : thm
val DISJOINT_DIFFS : thm
val DISJOINT_EMPTY : thm
val DISJOINT_EMPTY_REFL : thm
val DISJOINT_EMPTY_REFL_RWT : thm
val DISJOINT_IMAGE : thm
val DISJOINT_INSERT : thm
val DISJOINT_INSERT' : thm
val DISJOINT_SING_EMPTY : thm
val DISJOINT_SUBSET : thm
val DISJOINT_SUBSET' : thm
val DISJOINT_SYM : thm
val DISJOINT_UNION : thm
val DISJOINT_UNION' : thm
val DISJOINT_UNION_BOTH : thm
val ELT_IN_DELETE : thm
val EMPTY_DELETE : thm
val EMPTY_DIFF : thm
val EMPTY_FUNSET : thm
val EMPTY_IN_POW : thm
val EMPTY_NOT_IN_partition : thm
val EMPTY_NOT_UNIV : thm
val EMPTY_SUBSET : thm
val EMPTY_UNION : thm
val EMPTY_applied : thm
val ENUMERATE : thm
val EQUAL_SING : thm
val EQ_SUBSET_SUBSET : thm
val EQ_UNIV : thm
val EXISTS_IN_IMAGE : thm
val EXISTS_IN_INSERT : thm
val EXPLICIT_ENUMERATE_MONO : thm
val EXPLICIT_ENUMERATE_NOT_EMPTY : thm
val EXTENSION : thm
val EXTENSIONAL : thm
val EXTENSIONAL_EMPTY : thm
val EXTENSIONAL_EQ : thm
val EXTENSIONAL_UNIV : thm
val FINITELY_INJECTIVE_IMAGE_FINITE : thm
val FINITE_BIGINTER : thm
val FINITE_BIGUNION : thm
val FINITE_BIGUNION_EQ : thm
val FINITE_BIJ : thm
val FINITE_BIJ_CARD : thm
val FINITE_BIJ_CARD_EQ : thm
val FINITE_BIJ_COUNT : thm
val FINITE_BIJ_COUNT_EQ : thm
val FINITE_CARD_IMAGE : thm
val FINITE_COMPLETE_INDUCTION : thm
val FINITE_COUNT : thm
val FINITE_CROSS : thm
val FINITE_CROSS_EQ : thm
val FINITE_DELETE : thm
val FINITE_DIFF : thm
val FINITE_DIFF_down : thm
val FINITE_EMPTY : thm
val FINITE_HAS_SIZE : thm
val FINITE_IMAGE_INJ' : thm
val FINITE_IMAGE_INJ_EQ : thm
val FINITE_INDUCT : thm
val FINITE_INDUCT_STRONG : thm
val FINITE_INJ : thm
val FINITE_INSERT : thm
val FINITE_INTER : thm
val FINITE_ISO_NUM : thm
val FINITE_LEAST_MEASURE_INDUCTION : thm
val FINITE_POW : thm
val FINITE_POW_EQN : thm
val FINITE_PREIMAGE : thm
val FINITE_PRODUCT : thm
val FINITE_PRODUCT_DEPENDENT : thm
val FINITE_PSUBSET_INFINITE : thm
val FINITE_PSUBSET_UNIV : thm
val FINITE_REST : thm
val FINITE_REST_EQ : thm
val FINITE_RULES : thm
val FINITE_SING : thm
val FINITE_SURJ : thm
val FINITE_SURJ_BIJ : thm
val FINITE_StrongOrder_WF : thm
val FINITE_UNION : thm
val FINITE_WEAK_ENUMERATE : thm
val FINITE_WF_noloops : thm
val FINITE_is_measure_maximal : thm
val FINITE_partition : thm
val FINITE_partitions : thm
val FORALL_IN_BIGUNION : thm
val FORALL_IN_IMAGE : thm
val FORALL_IN_INSERT : thm
val FORALL_IN_UNION : thm
val FUNPOW_INJ : thm
val FUNPOW_eq_elim : thm
val FUNPOW_min_cancel : thm
val FUNSET_DFUNSET : thm
val FUNSET_EMPTY : thm
val FUNSET_INTER : thm
val FUNSET_THM : thm
val FUNSET_applied : thm
val GSPECIFICATION_applied : thm
val GSPEC_AND : thm
val GSPEC_EQ : thm
val GSPEC_EQ2 : thm
val GSPEC_ETA : thm
val GSPEC_F : thm
val GSPEC_F_COND : thm
val GSPEC_ID : thm
val GSPEC_IMAGE : thm
val GSPEC_OR : thm
val GSPEC_PAIR_ETA : thm
val GSPEC_T : thm
val HAS_SIZE_0 : thm
val HAS_SIZE_CARD : thm
val HAS_SIZE_IMAGE_INJ : thm
val HAS_SIZE_INDEX : thm
val HAS_SIZE_PRODUCT : thm
val HAS_SIZE_PRODUCT_DEPENDENT : thm
val HAS_SIZE_SUC : thm
val HAS_SIZE_UNION : thm
val IMAGE_11 : thm
val IMAGE_11_INFINITE : thm
val IMAGE_BIGUNION : thm
val IMAGE_CLAUSES : thm
val IMAGE_COMPOSE : thm
val IMAGE_CONG : thm
val IMAGE_CONST : thm
val IMAGE_DELETE : thm
val IMAGE_EMPTY : thm
val IMAGE_EQ_EMPTY : thm
val IMAGE_EQ_SING : thm
val IMAGE_FINITE : thm
val IMAGE_FST_CROSS : thm
val IMAGE_I : thm
val IMAGE_ID : thm
val IMAGE_II : thm
val IMAGE_IMAGE : thm
val IMAGE_IMAGE_partition : thm
val IMAGE_IN : thm
val IMAGE_INSERT : thm
val IMAGE_INTER : thm
val IMAGE_PREIMAGE : thm
val IMAGE_RESTRICTION : thm
val IMAGE_SING : thm
val IMAGE_SND_CROSS : thm
val IMAGE_SUBSET : thm
val IMAGE_SUBSET_gen : thm
val IMAGE_SURJ : thm
val IMAGE_UNION : thm
val IMAGE_applied : thm
val IMAGE_o : thm
val INFINITE_DIFF_FINITE : thm
val INFINITE_DIFF_FINITE' : thm
val INFINITE_EXPLICIT_ENUMERATE : thm
val INFINITE_INHAB : thm
val INFINITE_INJ : thm
val INFINITE_INJ_NOT_SURJ : thm
val INFINITE_NUM_UNIV : thm
val INFINITE_PAIR_UNIV : thm
val INFINITE_SUBSET : thm
val INFINITE_UNIV : thm
val INJECTIVE_IMAGE_FINITE : thm
val INJ_BIJ_SUBSET : thm
val INJ_CARD : thm
val INJ_CARD_IMAGE : thm
val INJ_CARD_IMAGE_EQ : thm
val INJ_COMPOSE : thm
val INJ_CONG : thm
val INJ_DELETE : thm
val INJ_ELEMENT : thm
val INJ_EMPTY : thm
val INJ_EQ_11 : thm
val INJ_EXTEND : thm
val INJ_I : thm
val INJ_ID : thm
val INJ_IFF : thm
val INJ_IMAGE : thm
val INJ_IMAGE_BIJ : thm
val INJ_IMAGE_DISJOINT : thm
val INJ_IMAGE_EQ : thm
val INJ_IMAGE_INTER : thm
val INJ_IMAGE_SUBSET : thm
val INJ_IMAGE_equiv_class : thm
val INJ_IMP_11 : thm
val INJ_INL : thm
val INJ_INR : thm
val INJ_INSERT : thm
val INJ_I_IMAGE : thm
val INJ_LINV_OPT : thm
val INJ_LINV_OPT_IMAGE : thm
val INJ_SUBSET : thm
val INJ_SUBSET_UNIV : thm
val INSERT_COMM : thm
val INSERT_DELETE : thm
val INSERT_DIFF : thm
val INSERT_EQ_SING : thm
val INSERT_INSERT : thm
val INSERT_INTER : thm
val INSERT_SING_UNION : thm
val INSERT_SUBSET : thm
val INSERT_UNION : thm
val INSERT_UNION_EQ : thm
val INSERT_UNIV : thm
val INSERT_applied : thm
val INTER_ASSOC : thm
val INTER_BIGUNION : thm
val INTER_COMM : thm
val INTER_CROSS : thm
val INTER_EMPTY : thm
val INTER_FINITE : thm
val INTER_IDEMPOT : thm
val INTER_OVER_UNION : thm
val INTER_SING : thm
val INTER_SUBSET : thm
val INTER_SUBSET_EQN : thm
val INTER_UNION : thm
val INTER_UNION_COMPL : thm
val INTER_UNIV : thm
val INTER_applied : thm
val IN_ABS : thm
val IN_APP : thm
val IN_BIGINTER : thm
val IN_BIGINTER_IMAGE : thm
val IN_BIGUNION : thm
val IN_BIGUNION_IMAGE : thm
val IN_COMPL : thm
val IN_COUNT : thm
val IN_CROSS : thm
val IN_DELETE : thm
val IN_DELETE_EQ : thm
val IN_DFUNSET : thm
val IN_DIFF : thm
val IN_DISJOINT : thm
val IN_EQ_UNIV_IMP : thm
val IN_FUNSET : thm
val IN_GSPEC : thm
val IN_GSPEC_IFF : thm
val IN_IMAGE : thm
val IN_INFINITE_NOT_FINITE : thm
val IN_INSERT : thm
val IN_INSERT_EXPAND : thm
val IN_INTER : thm
val IN_POW : thm
val IN_PREIMAGE : thm
val IN_REST : thm
val IN_SING : thm
val IN_UNION : thm
val IN_UNIV : thm
val IN_disjUNION : thm
val ITSET_CONG : thm
val ITSET_EMPTY : thm
val ITSET_IND : thm
val ITSET_INSERT : thm
val ITSET_PROPERTY : thm
val ITSET_REDUCTION : thm
val ITSET_SING : thm
val ITSET_THM : thm
val ITSET_def : thm
val K_SUBSET : thm
val KoenigsLemma : thm
val KoenigsLemma_WF : thm
val LESS_CARD_DIFF : thm
val LINV_DEF : thm
val LINV_OPT_THM : thm
val MAX_SET_ELIM : thm
val MAX_SET_EMPTY : thm
val MAX_SET_EQ_0 : thm
val MAX_SET_INTER : thm
val MAX_SET_IN_SET : thm
val MAX_SET_LESS : thm
val MAX_SET_PROPERTY : thm
val MAX_SET_REWRITES : thm
val MAX_SET_SING : thm
val MAX_SET_TEST : thm
val MAX_SET_TEST_IFF : thm
val MAX_SET_THM : thm
val MAX_SET_UNION : thm
val MEMBER_NOT_EMPTY : thm
val MIN_SET_ELIM : thm
val MIN_SET_EQ_0 : thm
val MIN_SET_IN_SET : thm
val MIN_SET_LEM : thm
val MIN_SET_LEQ_MAX_SET : thm
val MIN_SET_PROPERTY : thm
val MIN_SET_SING : thm
val MIN_SET_TEST : thm
val MIN_SET_TEST_IFF : thm
val MIN_SET_THM : thm
val MIN_SET_THM' : thm
val MIN_SET_UNION : thm
val NOT_EMPTY_INSERT : thm
val NOT_EMPTY_SING : thm
val NOT_EQUAL_SETS : thm
val NOT_INSERT_EMPTY : thm
val NOT_IN_EMPTY : thm
val NOT_IN_FINITE : thm
val NOT_PSUBSET_EMPTY : thm
val NOT_SING_EMPTY : thm
val NOT_UNIV_PSUBSET : thm
val NUM_2D_BIJ : thm
val NUM_2D_BIJ_BIG_SQUARE : thm
val NUM_2D_BIJ_INV : thm
val NUM_2D_BIJ_NZ : thm
val NUM_2D_BIJ_NZ_ALT : thm
val NUM_2D_BIJ_NZ_ALT2 : thm
val NUM_2D_BIJ_NZ_ALT2_INV : thm
val NUM_2D_BIJ_NZ_ALT_INV : thm
val NUM_2D_BIJ_NZ_INV : thm
val NUM_2D_BIJ_SMALL_SQUARE : thm
val NUM_SET_WOP : thm
val ONE_ELEMENT_SING : thm
val PAIR_IN_GSPEC_1 : thm
val PAIR_IN_GSPEC_2 : thm
val PAIR_IN_GSPEC_IFF : thm
val PAIR_IN_GSPEC_same : thm
val PHP : thm
val PI_CONSTANT : thm
val POW_EMPTY : thm
val POW_EQNS : thm
val POW_INSERT : thm
val POW_applied : thm
val PREIMAGE_ALT : thm
val PREIMAGE_BIGUNION : thm
val PREIMAGE_COMP : thm
val PREIMAGE_COMPL : thm
val PREIMAGE_COMPL_INTER : thm
val PREIMAGE_CROSS : thm
val PREIMAGE_DIFF : thm
val PREIMAGE_DISJOINT : thm
val PREIMAGE_EMPTY : thm
val PREIMAGE_I : thm
val PREIMAGE_IMAGE : thm
val PREIMAGE_INTER : thm
val PREIMAGE_K : thm
val PREIMAGE_SUBSET : thm
val PREIMAGE_UNION : thm
val PREIMAGE_UNIV : thm
val PREIMAGE_applied : thm
val PREIMAGE_o : thm
val PROD_IMAGE_CONG : thm
val PROD_IMAGE_CONSTANT : thm
val PROD_IMAGE_DELETE : thm
val PROD_IMAGE_EMPTY : thm
val PROD_IMAGE_EQ_0 : thm
val PROD_IMAGE_EQ_1 : thm
val PROD_IMAGE_INSERT : thm
val PROD_IMAGE_THM : thm
val PROD_SET_EMPTY : thm
val PROD_SET_IMAGE_REDUCTION : thm
val PROD_SET_INSERT : thm
val PROD_SET_THM : thm
val PSUBSET_EQN : thm
val PSUBSET_FINITE : thm
val PSUBSET_INSERT_SUBSET : thm
val PSUBSET_IRREFL : thm
val PSUBSET_MEMBER : thm
val PSUBSET_SING : thm
val PSUBSET_SUBSET_TRANS : thm
val PSUBSET_TRANS : thm
val PSUBSET_UNIV : thm
val RC_PSUBSET : thm
val RC_SUBSET_THM : thm
val REL_RESTRICT_EMPTY : thm
val REL_RESTRICT_SUBSET : thm
val RESTRICTION_COMPOSE : thm
val RESTRICTION_COMPOSE_LEFT : thm
val RESTRICTION_COMPOSE_RIGHT : thm
val RESTRICTION_EXTENSION : thm
val RESTRICTION_FIXPOINT : thm
val RESTRICTION_IDEMP : thm
val RESTRICTION_IN_EXTENSIONAL : thm
val RESTRICTION_RESTRICTION : thm
val RESTRICTION_UNIQUE : thm
val RESTRICTION_UNIQUE_ALT : thm
val REST_PSUBSET : thm
val REST_SING : thm
val REST_SUBSET : thm
val REST_applied : thm
val RINV_DEF : thm
val RTC_PSUBSET : thm
val RTC_SUBSET_THM : thm
val SCHROEDER_BERNSTEIN : thm
val SCHROEDER_BERNSTEIN_AUTO : thm
val SCHROEDER_CLOSE : thm
val SCHROEDER_CLOSED : thm
val SCHROEDER_CLOSE_SET : thm
val SCHROEDER_CLOSE_SUBSET : thm
val SET_CASES : thm
val SET_EQ_SUBSET : thm
val SET_MINIMUM : thm
val SIGMA_CARD_CONSTANT : thm
val SIGMA_CARD_SAME_SIZE_SETS : thm
val SIGMA_CONG : thm
val SIGMA_CONSTANT : thm
val SIGMA_LE_SIGMA : thm
val SIMPLE_FINITE_INDUCT : thm
val SING : thm
val SING_CARD_1 : thm
val SING_DELETE : thm
val SING_ELEMENT : thm
val SING_EMPTY : thm
val SING_FINITE : thm
val SING_IFF_CARD1 : thm
val SING_IFF_EMPTY_REST : thm
val SING_INSERT : thm
val SING_INTER : thm
val SING_ONE_ELEMENT : thm
val SING_TEST : thm
val SING_UNION : thm
val SING_applied : thm
val SING_partitions : thm
val SPECIFICATION : thm
val SUBSET_ADD : thm
val SUBSET_ANTISYM : thm
val SUBSET_ANTISYM_EQ : thm
val SUBSET_BIGINTER : thm
val SUBSET_BIGUNION : thm
val SUBSET_BIGUNION_I : thm
val SUBSET_BIGUNION_SUBSET_I : thm
val SUBSET_COMMUTING_ITSET_INSERT : thm
val SUBSET_COMMUTING_ITSET_RECURSES : thm
val SUBSET_COMMUTING_ITSET_REDUCTION : thm
val SUBSET_CROSS : thm
val SUBSET_DELETE : thm
val SUBSET_DELETE_BOTH : thm
val SUBSET_DIFF : thm
val SUBSET_DIFF_EMPTY : thm
val SUBSET_DISJOINT : thm
val SUBSET_EMPTY : thm
val SUBSET_EQ_CARD : thm
val SUBSET_FINITE : thm
val SUBSET_FINITE_I : thm
val SUBSET_IMAGE : thm
val SUBSET_INSERT : thm
val SUBSET_INSERT_DELETE : thm
val SUBSET_INSERT_RIGHT : thm
val SUBSET_INTER : thm
val SUBSET_INTER1 : thm
val SUBSET_INTER2 : thm
val SUBSET_INTER_ABSORPTION : thm
val SUBSET_K : thm
val SUBSET_MAX_SET : thm
val SUBSET_MIN_SET : thm
val SUBSET_OF_INSERT : thm
val SUBSET_POW : thm
val SUBSET_PSUBSET_TRANS : thm
val SUBSET_REFL : thm
val SUBSET_SING : thm
val SUBSET_THM : thm
val SUBSET_TRANS : thm
val SUBSET_UNION : thm
val SUBSET_UNION_ABSORPTION : thm
val SUBSET_UNIV : thm
val SUBSET_applied : thm
val SUBSET_count_MAX_SET : thm
val SUBSET_reflexive : thm
val SUBSET_transitive : thm
val SUM_IMAGE_ADD : thm
val SUM_IMAGE_CONG : thm
val SUM_IMAGE_CONSTANT : thm
val SUM_IMAGE_DELETE : thm
val SUM_IMAGE_DISJOINT : thm
val SUM_IMAGE_EMPTY : thm
val SUM_IMAGE_INJ_o : thm
val SUM_IMAGE_INSERT : thm
val SUM_IMAGE_IN_LE : thm
val SUM_IMAGE_MONO_LESS : thm
val SUM_IMAGE_MONO_LESS_EQ : thm
val SUM_IMAGE_MONO_LT : thm
val SUM_IMAGE_PERMUTES : thm
val SUM_IMAGE_SING : thm
val SUM_IMAGE_SUBSET_LE : thm
val SUM_IMAGE_THM : thm
val SUM_IMAGE_UNION : thm
val SUM_IMAGE_UNION_EQN : thm
val SUM_IMAGE_ZERO : thm
val SUM_IMAGE_lower_bound : thm
val SUM_IMAGE_upper_bound : thm
val SUM_SAME_IMAGE : thm
val SUM_SET_DELETE : thm
val SUM_SET_EMPTY : thm
val SUM_SET_INSERT : thm
val SUM_SET_IN_LE : thm
val SUM_SET_SING : thm
val SUM_SET_SUBSET_LE : thm
val SUM_SET_THM : thm
val SUM_SET_UNION : thm
val SUM_SET_count : thm
val SUM_SET_count_2 : thm
val SUM_UNIV : thm
val SURJECTIVE_IFF_INJECTIVE : thm
val SURJECTIVE_IFF_INJECTIVE_GEN : thm
val SURJ_CARD : thm
val SURJ_COMPOSE : thm
val SURJ_CONG : thm
val SURJ_ELEMENT : thm
val SURJ_EMPTY : thm
val SURJ_ID : thm
val SURJ_IMAGE : thm
val SURJ_IMP_INJ : thm
val SURJ_INJ_INV : thm
val TC_PSUBSET : thm
val TC_SUBSET_THM : thm
val UNION_ASSOC : thm
val UNION_COMM : thm
val UNION_DELETE : thm
val UNION_DIFF : thm
val UNION_DIFF_2 : thm
val UNION_DIFF_EQ : thm
val UNION_EMPTY : thm
val UNION_IDEMPOT : thm
val UNION_OVER_INTER : thm
val UNION_SUBSET : thm
val UNION_UNIV : thm
val UNION_applied : thm
val UNIQUE_MEMBER_SING : thm
val UNIV_BOOL : thm
val UNIV_FUNSET_UNIV : thm
val UNIV_FUN_TO_BOOL : thm
val UNIV_NOT_EMPTY : thm
val UNIV_SUBSET : thm
val UNIV_applied : thm
val X_LE_MAX_SET : thm
val bigunion_countable : thm
val chooser_compute : thm
val compl_insert : thm
val count_EQN : thm
val count_add : thm
val count_add1 : thm
val countable_EMPTY : thm
val countable_INSERT : thm
val countable_Uprod : thm
val countable_Usum : thm
val countable_image_nats : thm
val countable_surj : thm
val cross_countable : thm
val cross_countable_IFF : thm
val disjUNION_EQ_EMPTY : thm
val disjUNION_UNIV : thm
val disjointD : thm
val disjointI : thm
val disjoint_def : thm
val disjoint_empty : thm
val disjoint_image : thm
val disjoint_insert : thm
val disjoint_insert_imp : thm
val disjoint_insert_notin : thm
val disjoint_restrict : thm
val disjoint_same : thm
val disjoint_sing : thm
val disjoint_two : thm
val disjoint_union : thm
val empty_partitions : thm
val empty_refines : thm
val equiv_class_eq : thm
val equiv_on_subset : thm
val equivalence_same_part : thm
val finite_countable : thm
val image_countable : thm
val in_max_set : thm
val in_part : thm
val infinite_num_inj : thm
val infinite_pow_uncountable : thm
val infinite_rest : thm
val inj_countable : thm
val inj_image_countable_IFF : thm
val inj_surj : thm
val inter_countable : thm
val inv_image_equiv_on : thm
val is_measure_maximal_INSERT : thm
val is_measure_maximal_SING : thm
val num_FINITE : thm
val num_FINITE_AVOID : thm
val num_INFINITE : thm
val num_countable : thm
val pair_to_num_formula : thm
val pair_to_num_inv : thm
val pair_to_num_inv' : thm
val pairwise_EMPTY : thm
val pairwise_SUBSET : thm
val pairwise_UNION : thm
val part_SING : thm
val part_in_partition : thm
val part_partition : thm
val part_unique : thm
val partition_CARD : thm
val partition_SUBSET : thm
val partition_elements_disjoint : thm
val partition_elements_interrelate : thm
val partition_rel_eq : thm
val partitions_DISJOINT : thm
val partitions_FINITE : thm
val partitions_INSERT : thm
val partitions_PAIR_DISJOINT : thm
val partitions_SING : thm
val partitions_covers : thm
val partitions_empty : thm
val partitions_inj : thm
val partitions_thm : thm
val pow_no_surj : thm
val prime_PROD_IMAGE : thm
val refines_antisym : thm
val refines_grows_parts : thm
val refines_refl : thm
val refines_transitive : thm
val subset_countable : thm
val transitive_PSUBSET : thm
val union_countable : thm
val union_countable_IFF : thm
(*
[divides] Parent theory of "pred_set"
[numpair] Parent theory of "pred_set"
[BIGINTER] Definition
β’ βP. BIGINTER P = {x | βs. s β P β x β s}
[BIGUNION] Definition
β’ βP. BIGUNION P = {x | βs. s β P β§ x β s}
[BIJ_DEF] Definition
β’ βf s t. BIJ f s t β INJ f s t β§ SURJ f s t
[CARD_DEF] Definition
β’ CARD β
= 0 β§
βs. FINITE s β
βx. CARD (x INSERT s) = if x β s then CARD s else SUC (CARD s)
[CHOICE_DEF] Definition
β’ βs. s β β
β CHOICE s β s
[COMPL_DEF] Definition
β’ βP. COMPL P = π(:Ξ±) DIFF P
[CROSS_DEF] Definition
β’ βP Q. P Γ Q = {p | FST p β P β§ SND p β Q}
[DELETE_DEF] Definition
β’ βs x. s DELETE x = s DIFF {x}
[DFUNSET] Definition
β’ βP Q. DFUNSET P Q = (Ξ»f. βx. x β P β f x β Q x)
[DIFF_DEF] Definition
β’ βs t. s DIFF t = {x | x β s β§ x β t}
[DISJOINT_DEF] Definition
β’ βs t. DISJOINT s t β s β© t = β
[EMPTY_DEF] Definition
β’ β
= (Ξ»x. F)
[FINITE_DEF] Definition
β’ βs. FINITE s β βP. P β
β§ (βs. P s β βe. P (e INSERT s)) β P s
[FUNSET] Definition
β’ βP Q. FUNSET P Q = (Ξ»f. βx. x β P β f x β Q)
[GSPECIFICATION] Definition
β’ βf v. v β GSPEC f β βx. (v,T) = f x
[HAS_SIZE] Definition
β’ βs n. s HAS_SIZE n β FINITE s β§ CARD s = n
[IMAGE_DEF] Definition
β’ βf s. IMAGE f s = {f x | x β s}
[INJ_DEF] Definition
β’ βf s t.
INJ f s t β
(βx. x β s β f x β t) β§ βx y. x β s β§ y β s β f x = f y β x = y
[INSERT_DEF] Definition
β’ βx s. x INSERT s = {y | y = x β¨ y β s}
[INTER_DEF] Definition
β’ βs t. s β© t = {x | x β s β§ x β t}
[LINV_LO] Definition
β’ βf s y. LINV f s y = THE (LINV_OPT f s y)
[LINV_OPT_def] Definition
β’ βf s y.
LINV_OPT f s y =
if y β IMAGE f s then SOME (@x. x β s β§ f x = y) else NONE
[MAX_SET_DEF] Definition
β’ βs. FINITE s β
(s β β
β MAX_SET s β s β§ βy. y β s β y β€ MAX_SET s) β§
(s = β
β MAX_SET s = 0)
[MIN_SET_DEF] Definition
β’ MIN_SET = $LEAST
[POW_DEF] Definition
β’ βset. POW set = {s | s β set}
[PREIMAGE_def] Definition
β’ βf s. PREIMAGE f s = {x | f x β s}
[PROD_IMAGE_DEF] Definition
β’ βf s. Ξ f s = ITSET (Ξ»e acc. f e * acc) s 1
[PROD_SET_DEF] Definition
β’ PROD_SET = Ξ I
[PSUBSET_DEF] Definition
β’ βs t. s β t β s β t β§ s β t
[REL_RESTRICT_DEF] Definition
β’ βR s x y. REL_RESTRICT R s x y β x β s β§ y β s β§ R x y
[REST_DEF] Definition
β’ βs. REST s = s DELETE CHOICE s
[RINV_LO] Definition
β’ βf s y. RINV f s y = THE (LINV_OPT f s y)
[SING_DEF] Definition
β’ βs. SING s β βx. s = {x}
[SUBSET_DEF] Definition
β’ βs t. s β t β βx. x β s β x β t
[SUM_IMAGE_DEF] Definition
β’ βf s. β f s = ITSET (Ξ»e acc. f e + acc) s 0
[SUM_SET_DEF] Definition
β’ SUM_SET = β I
[SURJ_DEF] Definition
β’ βf s t.
SURJ f s t β
(βx. x β s β f x β t) β§ βx. x β t β βy. y β s β§ f y = x
[UNION_DEF] Definition
β’ βs t. s βͺ t = {x | x β s β¨ x β t}
[UNIV_DEF] Definition
β’ π(:Ξ±) = (Ξ»x. T)
[chooser_def] Definition
β’ (βs. chooser s 0 = CHOICE s) β§
βs n. chooser s (SUC n) = chooser (REST s) n
[closure_comm_assoc_fun_def] Definition
β’ βf s.
closure_comm_assoc_fun f s β
(βx y. x β s β§ y β s β f x y β s) β§
βx y z. x β s β§ y β s β§ z β s β f x (f y z) = f y (f x z)
[count_def] Definition
β’ βn. count n = {m | m < n}
[countable_def] Definition
β’ βs. countable s β βf. INJ f s π(:num)
[disjUNION_def] Definition
β’ βA B. A β B = {INL a | a β A} βͺ {INR b | b β B}
[disjoint] Definition
β’ disjoint = pairwise (RC DISJOINT)
[enumerate_def] Definition
β’ βs. enumerate s = @f. BIJ f π(:num) s
[equiv_on_def] Definition
β’ βR s.
R equiv_on s β
(βx. x β s β R x x) β§ (βx y. x β s β§ y β s β (R x y β R y x)) β§
βx y z. x β s β§ y β s β§ z β s β§ R x y β§ R y z β R x z
[is_measure_maximal_def] Definition
β’ βm s x. is_measure_maximal m s x β x β s β§ βy. y β s β m y β€ m x
[num_to_pair_def] Definition
β’ βn. num_to_pair n = (nfst n,nsnd n)
[pair_to_num_def] Definition
β’ βm n. pair_to_num (m,n) = m β n
[pairwise_def] Definition
β’ βP s. pairwise P s β βe1 e2. e1 β s β§ e2 β s β P e1 e2
[part_def] Definition
β’ βv x. part v x = @s. x β s β§ s β v
[partition_def] Definition
β’ βR s. partition R s = {t | βx. x β s β§ t = equiv_class R s x}
[partitions_def] Definition
β’ βX Y. X partitions Y β βR. R equiv_on Y β§ X = partition R Y
[refines_def] Definition
β’ βv1 v2. v1 refines v2 β βs1. s1 β v1 β βs2. s2 β v2 β§ s1 β s2
[schroeder_close_def] Definition
β’ βf s x. schroeder_close f s x β βn. x β FUNPOW (IMAGE f) n s
[ABSORPTION] Theorem
β’ βx s. x β s β x INSERT s = s
[ABSORPTION_RWT] Theorem
β’ βx s. x β s β x INSERT s = s
[ABS_DIFF_SUM_IMAGE] Theorem
β’ βs. FINITE s β
ABS_DIFF (β f s) (β g s) β€ β (Ξ»x. ABS_DIFF (f x) (g x)) s
[BIGINTER_2] Theorem
β’ βP Q. BIGINTER {P; Q} = P β© Q
[BIGINTER_EMPTY] Theorem
β’ BIGINTER β
= π(:Ξ±)
[BIGINTER_GSPEC] Theorem
β’ (βP f. BIGINTER {f x | P x} = {a | βx. P x β a β f x}) β§
(βP f. BIGINTER {f x y | P x y} = {a | βx y. P x y β a β f x y}) β§
βP f.
BIGINTER {f x y z | P x y z} =
{a | βx y z. P x y z β a β f x y z}
[BIGINTER_IMAGE] Theorem
β’ βf s. BIGINTER (IMAGE f s) = {y | βx. x β s β y β f x}
[BIGINTER_INSERT] Theorem
β’ βP B. BIGINTER (P INSERT B) = P β© BIGINTER B
[BIGINTER_INTER] Theorem
β’ βP Q. BIGINTER {P; Q} = P β© Q
[BIGINTER_SING] Theorem
β’ βP. BIGINTER {P} = P
[BIGINTER_SUBSET] Theorem
β’ βsp s t. t β s β§ t β sp β BIGINTER s β sp
[BIGINTER_UNION] Theorem
β’ βs1 s2. BIGINTER (s1 βͺ s2) = BIGINTER s1 β© BIGINTER s2
[BIGINTER_applied] Theorem
β’ BIGINTER B x β βP. P β B β x β P
[BIGUNION_CROSS] Theorem
β’ βf s t. BIGUNION (IMAGE f s) Γ t = BIGUNION (IMAGE (Ξ»n. f n Γ t) s)
[BIGUNION_EMPTY] Theorem
β’ BIGUNION β
= β
[BIGUNION_EQ_EMPTY] Theorem
β’ βP. (BIGUNION P = β
β P = β
β¨ P = {β
}) β§
(β
= BIGUNION P β P = β
β¨ P = {β
})
[BIGUNION_GSPEC] Theorem
β’ (βP f. BIGUNION {f x | P x} = {a | βx. P x β§ a β f x}) β§
(βP f. BIGUNION {f x y | P x y} = {a | βx y. P x y β§ a β f x y}) β§
βP f.
BIGUNION {f x y z | P x y z} =
{a | βx y z. P x y z β§ a β f x y z}
[BIGUNION_IMAGE] Theorem
β’ βf s. BIGUNION (IMAGE f s) = {y | βx. x β s β§ y β f x}
[BIGUNION_IMAGE_SUBSET] Theorem
β’ βf s t. BIGUNION (IMAGE f s) β t β βx. x β s β f x β t
[BIGUNION_IMAGE_UNIV] Theorem
β’ βf N.
(βn. N β€ n β f n = β
) β
BIGUNION (IMAGE f π(:num)) = BIGUNION (IMAGE f (count N))
[BIGUNION_INSERT] Theorem
β’ βs P. BIGUNION (s INSERT P) = s βͺ BIGUNION P
[BIGUNION_PAIR] Theorem
β’ βs t. BIGUNION {s; t} = s βͺ t
[BIGUNION_SING] Theorem
β’ βx. BIGUNION {x} = x
[BIGUNION_SUBSET] Theorem
β’ βX P. BIGUNION P β X β βY. Y β P β Y β X
[BIGUNION_UNION] Theorem
β’ βs1 s2. BIGUNION (s1 βͺ s2) = BIGUNION s1 βͺ BIGUNION s2
[BIGUNION_applied] Theorem
β’ βx sos. BIGUNION sos x β βs. x β s β§ s β sos
[BIGUNION_partition] Theorem
β’ R equiv_on s β BIGUNION (partition R s) = s
[BIJ_ALT] Theorem
β’ βf s t.
BIJ f s t β f β FUNSET s t β§ βy. y β t β β!x. x β s β§ y = f x
[BIJ_COMPOSE] Theorem
β’ βf g s t u. BIJ f s t β§ BIJ g t u β BIJ (g β f) s u
[BIJ_CONG] Theorem
β’ βf g s t. (βx. x β s β f x = g x) β (BIJ f s t β BIJ g s t)
[BIJ_DELETE] Theorem
β’ βs t f. BIJ f s t β βe. e β s β BIJ f (s DELETE e) (t DELETE f e)
[BIJ_ELEMENT] Theorem
β’ βf s t x. BIJ f s t β§ x β s β f x β t
[BIJ_EMPTY] Theorem
β’ βf. (βs. BIJ f β
s β s = β
) β§ βs. BIJ f s β
β s = β
[BIJ_FINITE] Theorem
β’ βf s t. BIJ f s t β§ FINITE s β FINITE t
[BIJ_FINITE_IFF] Theorem
β’ βf s t. BIJ f s t β (FINITE s β FINITE t)
[BIJ_FINITE_SUBSET] Theorem
β’ βf s t.
BIJ f π(:num) s β§ FINITE t β§ t β s β βN. βn. N β€ n β f n β t
[BIJ_ID] Theorem
β’ βs. (Ξ»x. x) PERMUTES s
[BIJ_IFF_INV] Theorem
β’ βf s t.
BIJ f s t β
(βx. x β s β f x β t) β§
βg. (βx. x β t β g x β s) β§ (βx. x β s β g (f x) = x) β§
βx. x β t β f (g x) = x
[BIJ_IMAGE] Theorem
β’ βf s t. BIJ f s t β t = IMAGE f s
[BIJ_IMAGE_partitions] Theorem
β’ βf x y v.
BIJ f x y β§ v partitions x β IMAGE (IMAGE f) v partitions y
[BIJ_IMP_11] Theorem
β’ BIJ f π(:Ξ±) π(:Ξ²) β βx y. f x = f y β x = y
[BIJ_INJ_SURJ] Theorem
β’ βs t. (βf. INJ f s t) β§ (βg. SURJ g s t) β βh. BIJ h s t
[BIJ_INSERT] Theorem
β’ βf e s t.
BIJ f (e INSERT s) t β
e β s β§ f e β t β§ BIJ f s (t DELETE f e) β¨ e β s β§ BIJ f s t
[BIJ_INSERT_IMP] Theorem
β’ βf e s t.
e β s β§ BIJ f (e INSERT s) t β
βu. f e INSERT u = t β§ f e β u β§ BIJ f s u
[BIJ_INV] Theorem
β’ βf s t.
BIJ f s t β
βg. BIJ g t s β§ (βx. x β s β (g β f) x = x) β§
βx. x β t β (f β g) x = x
[BIJ_IS_INJ] Theorem
β’ βf s t. BIJ f s t β βx y. x β s β§ y β s β§ f x = f y β x = y
[BIJ_IS_SURJ] Theorem
β’ βf s t. BIJ f s t β βx. x β t β βy. y β s β§ f y = x
[BIJ_I_SAME] Theorem
β’ βs. I PERMUTES s
[BIJ_LINV_BIJ] Theorem
β’ βf s t. BIJ f s t β BIJ (LINV f s) t s
[BIJ_LINV_INV] Theorem
β’ βf s t. BIJ f s t β βx. x β t β f (LINV f s x) = x
[BIJ_NUM_COUNTABLE] Theorem
β’ βs. (βf. BIJ f π(:num) s) β countable s
[BIJ_NUM_TO_PAIR] Theorem
β’ BIJ num_to_pair π(:num) (π(:num) Γ π(:num))
[BIJ_PAIR_TO_NUM] Theorem
β’ BIJ pair_to_num (π(:num) Γ π(:num)) π(:num)
[BIJ_SWAP] Theorem
β’ BIJ SWAP (π(:Ξ±) Γ π(:Ξ²)) (π(:Ξ²) Γ π(:Ξ±))
[BIJ_SYM] Theorem
β’ βs t. (βf. BIJ f s t) β βg. BIJ g t s
[BIJ_SYM_IMP] Theorem
β’ βs t. (βf. BIJ f s t) β βg. BIJ g t s
[BIJ_THM] Theorem
β’ βf s t.
BIJ f s t β
(βx. x β s β f x β t) β§ βy. y β t β β!x. x β s β§ f x = y
[BIJ_TRANS] Theorem
β’ βs t u. (βf. BIJ f s t) β§ (βg. BIJ g t u) β βh. BIJ h s u
[BIJ_support] Theorem
β’ βf s' s.
f PERMUTES s' β§ s' β s β§ (βx. x β s' β f x = x) β f PERMUTES s
[CARD_AS_SIGMA] Theorem
β’ βs. FINITE s β CARD s = β (Ξ»x. 1) s
[CARD_BIGUNION_SAME_SIZED_SETS] Theorem
β’ βn s.
FINITE s β§ (βe. e β s β FINITE e β§ CARD e = n) β§
(βe1 e2. e1 β s β§ e2 β s β§ e1 β e2 β DISJOINT e1 e2) β
CARD (BIGUNION s) = CARD s * n
[CARD_CLAUSES] Theorem
β’ CARD β
= 0 β§
βs. FINITE s β
βx. CARD (x INSERT s) = if x β s then CARD s else SUC (CARD s)
[CARD_COUNT] Theorem
β’ βn. CARD (count n) = n
[CARD_CROSS] Theorem
β’ βP Q. FINITE P β§ FINITE Q β CARD (P Γ Q) = CARD P * CARD Q
[CARD_DELETE] Theorem
β’ βs. FINITE s β
βx. CARD (s DELETE x) = if x β s then CARD s β 1 else CARD s
[CARD_DIFF] Theorem
β’ βt. FINITE t β
βs. FINITE s β CARD (s DIFF t) = CARD s β CARD (s β© t)
[CARD_DIFF_EQN] Theorem
β’ βt s. FINITE s β CARD (s DIFF t) = CARD s β CARD (s β© t)
[CARD_EMPTY] Theorem
β’ CARD β
= 0
[CARD_EQ_0] Theorem
β’ βs. FINITE s β (CARD s = 0 β s = β
)
[CARD_EQ_SIGMA] Theorem
β’ βs. FINITE s β CARD s = β (K 1) s
[CARD_IMAGE] Theorem
β’ βs. FINITE s β CARD (IMAGE f s) β€ CARD s
[CARD_IMAGE_INJ] Theorem
β’ βf s.
(βx y. x β s β§ y β s β§ f x = f y β x = y) β§ FINITE s β
CARD (IMAGE f s) = CARD s
[CARD_IMAGE_LE] Theorem
β’ βf s. FINITE s β CARD (IMAGE f s) β€ CARD s
[CARD_IMAGE_SUC] Theorem
β’ βs. FINITE s β CARD (IMAGE SUC s) = CARD s
[CARD_INJ_IMAGE] Theorem
β’ βf s.
(βx y. f x = f y β x = y) β§ FINITE s β CARD (IMAGE f s) = CARD s
[CARD_INSERT] Theorem
β’ βs. FINITE s β
βx. CARD (x INSERT s) = if x β s then CARD s else SUC (CARD s)
[CARD_INTER_LESS_EQ] Theorem
β’ βs. FINITE s β βt. CARD (s β© t) β€ CARD s
[CARD_LE_MAX_SET] Theorem
β’ FINITE s β CARD s β€ MAX_SET s + 1
[CARD_POW] Theorem
β’ βs. FINITE s β CARD (POW s) = 2 ** CARD s
[CARD_PRODUCT] Theorem
β’ βs t.
FINITE s β§ FINITE t β
CARD {(x,y) | x β s β§ y β t} = CARD s * CARD t
[CARD_PSUBSET] Theorem
β’ βs. FINITE s β βt. t β s β CARD t < CARD s
[CARD_REST] Theorem
β’ βs. FINITE s β§ s β β
β CARD (REST s) = CARD s β 1
[CARD_SING] Theorem
β’ βx. CARD {x} = 1
[CARD_SING_CROSS] Theorem
β’ βx P. FINITE P β CARD ({x} Γ P) = CARD P
[CARD_SUBSET] Theorem
β’ βs. FINITE s β βt. t β s β CARD t β€ CARD s
[CARD_UNION] Theorem
β’ βs. FINITE s β
βt. FINITE t β CARD (s βͺ t) + CARD (s β© t) = CARD s + CARD t
[CARD_UNION_DISJOINT] Theorem
β’ βs t.
FINITE s β§ FINITE t β§ DISJOINT s t β
CARD (s βͺ t) = CARD s + CARD t
[CARD_UNION_EQN] Theorem
β’ βs t.
FINITE s β§ FINITE t β
CARD (s βͺ t) = CARD s + CARD t β CARD (s β© t)
[CARD_UNION_LE] Theorem
β’ FINITE s β§ FINITE t β CARD (s βͺ t) β€ CARD s + CARD t
[CARD_disjUNION] Theorem
β’ FINITE s β§ FINITE t β CARD (s β t) = CARD s + CARD t
[CHOICE_INSERT_REST] Theorem
β’ βs. s β β
β CHOICE s INSERT REST s = s
[CHOICE_INTRO] Theorem
β’ (βx. x β s) β§ (βx. x β s β P x) β P (CHOICE s)
[CHOICE_NOT_IN_REST] Theorem
β’ βs. CHOICE s β REST s
[CHOICE_SING] Theorem
β’ βx. CHOICE {x} = x
[COMMUTING_ITSET_INSERT] Theorem
β’ βf s.
(βx y z. f x (f y z) = f y (f x z)) β§ FINITE s β
βx b. ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b)
[COMMUTING_ITSET_RECURSES] Theorem
β’ βf e s b.
(βx y z. f x (f y z) = f y (f x z)) β§ FINITE s β
ITSET f (e INSERT s) b = f e (ITSET f (s DELETE e) b)
[COMPL_CLAUSES] Theorem
β’ βs. COMPL s β© s = β
β§ COMPL s βͺ s = π(:Ξ±)
[COMPL_COMPL] Theorem
β’ βs. COMPL (COMPL s) = s
[COMPL_EMPTY] Theorem
β’ COMPL β
= π(:Ξ±)
[COMPL_INTER] Theorem
β’ x β© COMPL x = β
β§ COMPL x β© x = β
[COMPL_SPLITS] Theorem
β’ βp q. p β© q βͺ COMPL p β© q = q
[COMPL_UNION] Theorem
β’ COMPL (s βͺ t) = COMPL s β© COMPL t
[COMPL_applied] Theorem
β’ βx s. COMPL s x β x β s
[COMPONENT] Theorem
β’ βx s. x β x INSERT s
[COUNTABLE_ALT] Theorem
β’ βs. countable s β βf. βx. x β s β βn. f n = x
[COUNTABLE_ALT_BIJ] Theorem
β’ βs. countable s β FINITE s β¨ BIJ (enumerate s) π(:num) s
[COUNTABLE_COUNT] Theorem
β’ βn. countable (count n)
[COUNTABLE_ENUM] Theorem
β’ βc. countable c β c = β
β¨ βf. c = IMAGE f π(:num)
[COUNTABLE_IMAGE_NUM] Theorem
β’ βf s. countable (IMAGE f s)
[COUNTABLE_NUM] Theorem
β’ βs. countable s
[COUNTABLE_SUBSET] Theorem
β’ βs t. s β t β§ countable t β countable s
[COUNT_11] Theorem
β’ βn1 n2. count n1 = count n2 β n1 = n2
[COUNT_DELETE] Theorem
β’ βn. count n DELETE n = count n
[COUNT_EQ_EMPTY] Theorem
β’ count n = β
β n = 0
[COUNT_MONO] Theorem
β’ βm n. m β€ n β count m β count n
[COUNT_NOT_EMPTY] Theorem
β’ βn. 0 < n β count n β β
[COUNT_ONE] Theorem
β’ count 1 = {0}
[COUNT_SUC] Theorem
β’ βn. count (SUC n) = n INSERT count n
[COUNT_ZERO] Theorem
β’ count 0 = β
[COUNT_applied] Theorem
β’ βm n. count n m β m < n
[CROSS_BIGUNION] Theorem
β’ βf s t. s Γ BIGUNION (IMAGE f t) = BIGUNION (IMAGE (Ξ»n. s Γ f n) t)
[CROSS_EMPTY] Theorem
β’ βP. P Γ β
= β
β§ β
Γ P = β
[CROSS_EMPTY_EQN] Theorem
β’ s Γ t = β
β s = β
β¨ t = β
[CROSS_EQNS] Theorem
β’ βs1 s2.
β
Γ s2 = β
β§ (a INSERT s1) Γ s2 = IMAGE (Ξ»y. (a,y)) s2 βͺ s1 Γ s2
[CROSS_INSERT_LEFT] Theorem
β’ βP Q x. (x INSERT P) Γ Q = {x} Γ Q βͺ P Γ Q
[CROSS_INSERT_RIGHT] Theorem
β’ βP Q x. P Γ (x INSERT Q) = P Γ {x} βͺ P Γ Q
[CROSS_SINGS] Theorem
β’ βx y. {x} Γ {y} = {(x,y)}
[CROSS_SUBSET] Theorem
β’ βP Q P0 Q0. P0 Γ Q0 β P Γ Q β P0 = β
β¨ Q0 = β
β¨ P0 β P β§ Q0 β Q
[CROSS_UNIV] Theorem
β’ π(:Ξ± # Ξ²) = π(:Ξ±) Γ π(:Ξ²)
[CROSS_applied] Theorem
β’ βP Q x. (P Γ Q) x β FST x β P β§ SND x β Q
[DECOMPOSITION] Theorem
β’ βs x. x β s β βt. s = x INSERT t β§ x β t
[DELETE_COMM] Theorem
β’ βx y s. s DELETE x DELETE y = s DELETE y DELETE x
[DELETE_DELETE] Theorem
β’ βx s. s DELETE x DELETE x = s DELETE x
[DELETE_EQ_SING] Theorem
β’ βs x. x β s β (s DELETE x = β
β s = {x})
[DELETE_INSERT] Theorem
β’ βx y s.
(x INSERT s) DELETE y =
if x = y then s DELETE y else x INSERT s DELETE y
[DELETE_INTER] Theorem
β’ βs t x. (s DELETE x) β© t = s β© t DELETE x
[DELETE_NON_ELEMENT] Theorem
β’ βx s. x β s β s DELETE x = s
[DELETE_NON_ELEMENT_RWT] Theorem
β’ βs x. x β s β s DELETE x = s
[DELETE_SUBSET] Theorem
β’ βx s. s DELETE x β s
[DELETE_SUBSET_INSERT] Theorem
β’ βs e s2. s DELETE e β s2 β s β e INSERT s2
[DELETE_applied] Theorem
β’ βs x y. (s DELETE y) x β x β s β§ x β y
[DFUNSET_applied] Theorem
β’ βf P Q. DFUNSET P Q f β βx. x β P β f x β Q x
[DIFF_BIGINTER] Theorem
β’ βsp s.
(βt. t β s β t β sp) β§ s β β
β
BIGINTER s = sp DIFF BIGUNION (IMAGE (Ξ»u. sp DIFF u) s)
[DIFF_BIGINTER1] Theorem
β’ βsp s. sp DIFF BIGINTER s = BIGUNION (IMAGE (Ξ»u. sp DIFF u) s)
[DIFF_COMM] Theorem
β’ βx y z. x DIFF y DIFF z = x DIFF z DIFF y
[DIFF_DIFF] Theorem
β’ βs t. s DIFF t DIFF t = s DIFF t
[DIFF_DIFF_SUBSET] Theorem
β’ βs t. t β s β s DIFF (s DIFF t) = t
[DIFF_EMPTY] Theorem
β’ βs. s DIFF β
= s
[DIFF_EQ_EMPTY] Theorem
β’ βs. s DIFF s = β
[DIFF_INSERT] Theorem
β’ βs t x. s DIFF (x INSERT t) = s DELETE x DIFF t
[DIFF_INTER] Theorem
β’ βs t g. (s DIFF t) β© g = s β© g DIFF t
[DIFF_INTER2] Theorem
β’ βs t. s DIFF t β© s = s DIFF t
[DIFF_INTER_COMPL] Theorem
β’ βs t. s DIFF t = s β© COMPL t
[DIFF_INTER_SUBSET] Theorem
β’ βr s t. r β s β r DIFF s β© t = r DIFF t
[DIFF_SAME_UNION] Theorem
β’ βx y. x βͺ y DIFF x = y DIFF x β§ x βͺ y DIFF y = x DIFF y
[DIFF_SUBSET] Theorem
β’ βs t. s DIFF t β s
[DIFF_UNION] Theorem
β’ βx y z. x DIFF (y βͺ z) = x DIFF y DIFF z
[DIFF_UNIV] Theorem
β’ βs. s DIFF π(:Ξ±) = β
[DIFF_applied] Theorem
β’ βs t x. (s DIFF t) x β x β s β§ x β t
[DISJOINT_ALT] Theorem
β’ βs t. DISJOINT s t β βx. x β s β x β t
[DISJOINT_ALT'] Theorem
β’ βs t. DISJOINT s t β βx. x β t β x β s
[DISJOINT_BIGINTER] Theorem
β’ βX Y P.
Y β P β§ DISJOINT Y X β
DISJOINT X (BIGINTER P) β§ DISJOINT (BIGINTER P) X
[DISJOINT_BIGUNION] Theorem
β’ (βs t. DISJOINT (BIGUNION s) t β βs'. s' β s β DISJOINT s' t) β§
βs t. DISJOINT t (BIGUNION s) β βs'. s' β s β DISJOINT t s'
[DISJOINT_COUNT] Theorem
β’ βf. (βm n. m β n β DISJOINT (f m) (f n)) β
βn. DISJOINT (f n) (BIGUNION (IMAGE f (count n)))
[DISJOINT_DELETE_SYM] Theorem
β’ βs t x. DISJOINT (s DELETE x) t β DISJOINT (t DELETE x) s
[DISJOINT_DIFF] Theorem
β’ βs t. DISJOINT t (s DIFF t) β§ DISJOINT (s DIFF t) t
[DISJOINT_DIFFS] Theorem
β’ βf g m n.
(βn. f n β f (SUC n)) β§ (βn. g n = f (SUC n) DIFF f n) β§ m β n β
DISJOINT (g m) (g n)
[DISJOINT_EMPTY] Theorem
β’ βs. DISJOINT β
s β§ DISJOINT s β
[DISJOINT_EMPTY_REFL] Theorem
β’ βs. s = β
β DISJOINT s s
[DISJOINT_EMPTY_REFL_RWT] Theorem
β’ βs. DISJOINT s s β s = β
[DISJOINT_IMAGE] Theorem
β’ (βx y. f x = f y β x = y) β
(DISJOINT (IMAGE f s1) (IMAGE f s2) β DISJOINT s1 s2)
[DISJOINT_INSERT] Theorem
β’ βx s t. DISJOINT (x INSERT s) t β DISJOINT s t β§ x β t
[DISJOINT_INSERT'] Theorem
β’ βx s t. DISJOINT t (x INSERT s) β DISJOINT t s β§ x β t
[DISJOINT_SING_EMPTY] Theorem
β’ βx. DISJOINT {x} β
[DISJOINT_SUBSET] Theorem
β’ βs t u. DISJOINT s t β§ u β t β DISJOINT s u
[DISJOINT_SUBSET'] Theorem
β’ βs t u. DISJOINT s t β§ u β s β DISJOINT u t
[DISJOINT_SYM] Theorem
β’ βs t. DISJOINT s t β DISJOINT t s
[DISJOINT_UNION] Theorem
β’ βs t u. DISJOINT (s βͺ t) u β DISJOINT s u β§ DISJOINT t u
[DISJOINT_UNION'] Theorem
β’ βs t u. DISJOINT u (s βͺ t) β DISJOINT u s β§ DISJOINT u t
[DISJOINT_UNION_BOTH] Theorem
β’ βs t u.
(DISJOINT (s βͺ t) u β DISJOINT s u β§ DISJOINT t u) β§
(DISJOINT u (s βͺ t) β DISJOINT s u β§ DISJOINT t u)
[ELT_IN_DELETE] Theorem
β’ βx s. x β s DELETE x
[EMPTY_DELETE] Theorem
β’ βx. β
DELETE x = β
[EMPTY_DIFF] Theorem
β’ βs. β
DIFF s = β
[EMPTY_FUNSET] Theorem
β’ βs. FUNSET β
s = π(:Ξ± -> Ξ²)
[EMPTY_IN_POW] Theorem
β’ βs. β
β POW s
[EMPTY_NOT_IN_partition] Theorem
β’ R equiv_on s β β
β partition R s
[EMPTY_NOT_UNIV] Theorem
β’ β
β π(:Ξ±)
[EMPTY_SUBSET] Theorem
β’ βs. β
β s
[EMPTY_UNION] Theorem
β’ βs t. s βͺ t = β
β s = β
β§ t = β
[EMPTY_applied] Theorem
β’ β
x β F
[ENUMERATE] Theorem
β’ βs. (βf. BIJ f π(:num) s) β BIJ (enumerate s) π(:num) s
[EQUAL_SING] Theorem
β’ βx y. {x} = {y} β x = y
[EQ_SUBSET_SUBSET] Theorem
β’ βs t. s = t β s β t β§ t β s
[EQ_UNIV] Theorem
β’ (βx. x β s) β s = π(:Ξ±)
[EXISTS_IN_IMAGE] Theorem
β’ βP f s. (βy. y β IMAGE f s β§ P y) β βx. x β s β§ P (f x)
[EXISTS_IN_INSERT] Theorem
β’ βP a s. (βx. x β a INSERT s β§ P x) β P a β¨ βx. x β s β§ P x
[EXPLICIT_ENUMERATE_MONO] Theorem
β’ βn s. FUNPOW REST n s β s
[EXPLICIT_ENUMERATE_NOT_EMPTY] Theorem
β’ βn s. INFINITE s β FUNPOW REST n s β β
[EXTENSION] Theorem
β’ βs t. s = t β βx. x β s β x β t
[EXTENSIONAL] Theorem
β’ βs. EXTENSIONAL s = {f | βx. x β s β f x = ARB}
[EXTENSIONAL_EMPTY] Theorem
β’ EXTENSIONAL β
= {(Ξ»x. ARB)}
[EXTENSIONAL_EQ] Theorem
β’ βs f g.
f β EXTENSIONAL s β§ g β EXTENSIONAL s β§ (βx. x β s β f x = g x) β
f = g
[EXTENSIONAL_UNIV] Theorem
β’ βf. EXTENSIONAL π(:Ξ±) f
[FINITELY_INJECTIVE_IMAGE_FINITE] Theorem
β’ βf. (βx. FINITE {y | x = f y}) β βs. FINITE (IMAGE f s) β FINITE s
[FINITE_BIGINTER] Theorem
β’ (βs. s β P β§ FINITE s) β FINITE (BIGINTER P)
[FINITE_BIGUNION] Theorem
β’ βP. FINITE P β§ (βs. s β P β FINITE s) β FINITE (BIGUNION P)
[FINITE_BIGUNION_EQ] Theorem
β’ βP. FINITE (BIGUNION P) β FINITE P β§ βs. s β P β FINITE s
[FINITE_BIJ] Theorem
β’ βf s t. FINITE s β§ BIJ f s t β FINITE t β§ CARD s = CARD t
[FINITE_BIJ_CARD] Theorem
β’ βf s t. FINITE s β§ BIJ f s t β CARD s = CARD t
[FINITE_BIJ_CARD_EQ] Theorem
β’ βS. FINITE S β βt f. BIJ f S t β§ FINITE t β CARD S = CARD t
[FINITE_BIJ_COUNT] Theorem
β’ βs. FINITE s β βf b. BIJ f (count b) s
[FINITE_BIJ_COUNT_EQ] Theorem
β’ βs. FINITE s β βc n. BIJ c (count n) s
[FINITE_CARD_IMAGE] Theorem
β’ βs f.
(βx y. f x = f y β x = y) β§ FINITE s β CARD (IMAGE f s) = CARD s
[FINITE_COMPLETE_INDUCTION] Theorem
β’ βP. (βx. (βy. y β x β P y) β FINITE x β P x) β βx. FINITE x β P x
[FINITE_COUNT] Theorem
β’ βn. FINITE (count n)
[FINITE_CROSS] Theorem
β’ βP Q. FINITE P β§ FINITE Q β FINITE (P Γ Q)
[FINITE_CROSS_EQ] Theorem
β’ βP Q. FINITE (P Γ Q) β P = β
β¨ Q = β
β¨ FINITE P β§ FINITE Q
[FINITE_DELETE] Theorem
β’ βx s. FINITE (s DELETE x) β FINITE s
[FINITE_DIFF] Theorem
β’ βs. FINITE s β βt. FINITE (s DIFF t)
[FINITE_DIFF_down] Theorem
β’ βP Q. FINITE (P DIFF Q) β§ FINITE Q β FINITE P
[FINITE_EMPTY] Theorem
β’ FINITE β
[FINITE_HAS_SIZE] Theorem
β’ βs. FINITE s β s HAS_SIZE CARD s
[FINITE_IMAGE_INJ'] Theorem
β’ (βx y. x β s β§ y β s β (f x = f y β x = y)) β
(FINITE (IMAGE f s) β FINITE s)
[FINITE_IMAGE_INJ_EQ] Theorem
β’ βf s.
(βx y. x β s β§ y β s β§ f x = f y β x = y) β
(FINITE (IMAGE f s) β FINITE s)
[FINITE_INDUCT] Theorem
β’ βP. P β
β§ (βs. FINITE s β§ P s β βe. e β s β P (e INSERT s)) β
βs. FINITE s β P s
[FINITE_INDUCT_STRONG] Theorem
β’ βP. P β
β§ (βx s. P s β§ x β s β§ FINITE s β P (x INSERT s)) β
βs. FINITE s β P s
[FINITE_INJ] Theorem
β’ βf s t. INJ f s t β§ FINITE t β FINITE s
[FINITE_INSERT] Theorem
β’ βx s. FINITE (x INSERT s) β FINITE s
[FINITE_INTER] Theorem
β’ βs1 s2. FINITE s1 β¨ FINITE s2 β FINITE (s1 β© s2)
[FINITE_ISO_NUM] Theorem
β’ βs. FINITE s β
βf. (βn m. n < CARD s β§ m < CARD s β f n = f m β n = m) β§
s = {f n | n < CARD s}
[FINITE_LEAST_MEASURE_INDUCTION] Theorem
β’ βf P.
P β
β§
(βa s. a β s β§ (βb. b β s β f a β€ f b) β§ P s β P (a INSERT s)) β
βs. FINITE s β P s
[FINITE_POW] Theorem
β’ βs. FINITE s β FINITE (POW s)
[FINITE_POW_EQN] Theorem
β’ FINITE (POW s) β FINITE s
[FINITE_PREIMAGE] Theorem
β’ (βx y. f x = f y β x = y) β§ FINITE s β FINITE (PREIMAGE f s)
[FINITE_PRODUCT] Theorem
β’ βs t. FINITE s β§ FINITE t β FINITE {(x,y) | x β s β§ y β t}
[FINITE_PRODUCT_DEPENDENT] Theorem
β’ βf s t.
FINITE s β§ (βx. x β s β FINITE (t x)) β
FINITE {f x y | x β s β§ y β t x}
[FINITE_PSUBSET_INFINITE] Theorem
β’ βs. INFINITE s β βt. FINITE t β t β s β t β s
[FINITE_PSUBSET_UNIV] Theorem
β’ INFINITE π(:Ξ±) β βs. FINITE s β s β π(:Ξ±)
[FINITE_REST] Theorem
β’ βs. FINITE s β FINITE (REST s)
[FINITE_REST_EQ] Theorem
β’ βs. FINITE (REST s) β FINITE s
[FINITE_RULES] Theorem
β’ FINITE β
β§ βs. FINITE s β βx. FINITE (x INSERT s)
[FINITE_SING] Theorem
β’ βx. FINITE {x}
[FINITE_SURJ] Theorem
β’ FINITE s β§ SURJ f s t β FINITE t
[FINITE_SURJ_BIJ] Theorem
β’ FINITE s β§ SURJ f s t β§ CARD t = CARD s β BIJ f s t
[FINITE_StrongOrder_WF] Theorem
β’ βR s.
FINITE s β§ StrongOrder (REL_RESTRICT R s) β WF (REL_RESTRICT R s)
[FINITE_UNION] Theorem
β’ βs t. FINITE (s βͺ t) β FINITE s β§ FINITE t
[FINITE_WEAK_ENUMERATE] Theorem
β’ βs. FINITE s β βf b. βe. e β s β βn. n < b β§ e = f n
[FINITE_WF_noloops] Theorem
β’ βs. FINITE s β
(WF (REL_RESTRICT R s) β irreflexive (REL_RESTRICT R s)βΊ)
[FINITE_is_measure_maximal] Theorem
β’ βm s. FINITE s β§ s β β
β βx. is_measure_maximal m s x
[FINITE_partition] Theorem
β’ βR s.
FINITE s β
FINITE (partition R s) β§ βt. t β partition R s β FINITE t
[FINITE_partitions] Theorem
β’ βx. FINITE x β FINITE {v | v partitions x}
[FORALL_IN_BIGUNION] Theorem
β’ βP s. (βx. x β BIGUNION s β P x) β βt x. t β s β§ x β t β P x
[FORALL_IN_IMAGE] Theorem
β’ βP f s. (βy. y β IMAGE f s β P y) β βx. x β s β P (f x)
[FORALL_IN_INSERT] Theorem
β’ βP a s. (βx. x β a INSERT s β P x) β P a β§ βx. x β s β P x
[FORALL_IN_UNION] Theorem
β’ βP s t. (βx. x β s βͺ t β P x) β (βx. x β s β P x) β§ βx. x β t β P x
[FUNPOW_INJ] Theorem
β’ INJ f π(:Ξ±) π(:Ξ±) β INJ (FUNPOW f n) π(:Ξ±) π(:Ξ±)
[FUNPOW_eq_elim] Theorem
β’ INJ f π(:Ξ±) π(:Ξ±) β (FUNPOW f n t = FUNPOW f n t' β t = t')
[FUNPOW_min_cancel] Theorem
β’ n β€ n' β§ INJ f π(:Ξ±) π(:Ξ±) β
(FUNPOW f n X = FUNPOW f n' X' β X = FUNPOW f (n' β n) X')
[FUNSET_DFUNSET] Theorem
β’ βx y. FUNSET x y = DFUNSET x (K y)
[FUNSET_EMPTY] Theorem
β’ βs f. f β FUNSET s β
β s = β
[FUNSET_INTER] Theorem
β’ βa b c. FUNSET a (b β© c) = FUNSET a b β© FUNSET a c
[FUNSET_THM] Theorem
β’ βs t f x. f β FUNSET s t β§ x β s β f x β t
[FUNSET_applied] Theorem
β’ βf P Q. FUNSET P Q f β βx. x β P β f x β Q
[GSPECIFICATION_applied] Theorem
β’ βf v. GSPEC f v β βx. (v,T) = f x
[GSPEC_AND] Theorem
β’ βP Q. {x | P x β§ Q x} = {x | P x} β© {x | Q x}
[GSPEC_EQ] Theorem
β’ {x | x = y} = {y}
[GSPEC_EQ2] Theorem
β’ {x | y = x} = {y}
[GSPEC_ETA] Theorem
β’ {x | P x} = P
[GSPEC_F] Theorem
β’ {x | F} = β
[GSPEC_F_COND] Theorem
β’ βf. (βx. Β¬SND (f x)) β GSPEC f = β
[GSPEC_ID] Theorem
β’ {x | x β y} = y
[GSPEC_IMAGE] Theorem
β’ GSPEC f = IMAGE (FST β f) (SND β f)
[GSPEC_OR] Theorem
β’ βP Q. {x | P x β¨ Q x} = {x | P x} βͺ {x | Q x}
[GSPEC_PAIR_ETA] Theorem
β’ {(x,y) | P x y} = UNCURRY P
[GSPEC_T] Theorem
β’ {x | T} = π(:Ξ±)
[HAS_SIZE_0] Theorem
β’ βs. s HAS_SIZE 0 β s = β
[HAS_SIZE_CARD] Theorem
β’ βs n. s HAS_SIZE n β CARD s = n
[HAS_SIZE_IMAGE_INJ] Theorem
β’ βf s n.
(βx y. x β s β§ y β s β§ f x = f y β x = y) β§ s HAS_SIZE n β
IMAGE f s HAS_SIZE n
[HAS_SIZE_INDEX] Theorem
β’ βs n.
s HAS_SIZE n β
βf. (βm. m < n β f m β s) β§ βx. x β s β β!m. m < n β§ f m = x
[HAS_SIZE_PRODUCT] Theorem
β’ βs m t n.
s HAS_SIZE m β§ t HAS_SIZE n β
{(x,y) | x β s β§ y β t} HAS_SIZE m * n
[HAS_SIZE_PRODUCT_DEPENDENT] Theorem
β’ βs m t n.
s HAS_SIZE m β§ (βx. x β s β t x HAS_SIZE n) β
{(x,y) | x β s β§ y β t x} HAS_SIZE m * n
[HAS_SIZE_SUC] Theorem
β’ βs n. s HAS_SIZE SUC n β s β β
β§ βa. a β s β s DELETE a HAS_SIZE n
[HAS_SIZE_UNION] Theorem
β’ βs t m n.
s HAS_SIZE m β§ t HAS_SIZE n β§ DISJOINT s t β s βͺ t HAS_SIZE m + n
[IMAGE_11] Theorem
β’ (βx y. f x = f y β x = y) β (IMAGE f s1 = IMAGE f s2 β s1 = s2)
[IMAGE_11_INFINITE] Theorem
β’ βf. (βx y. f x = f y β x = y) β
βs. INFINITE s β INFINITE (IMAGE f s)
[IMAGE_BIGUNION] Theorem
β’ βf M. IMAGE f (BIGUNION M) = BIGUNION (IMAGE (IMAGE f) M)
[IMAGE_CLAUSES] Theorem
β’ (βf. IMAGE f β
= β
) β§
βf x s. IMAGE f (x INSERT s) = f x INSERT IMAGE f s
[IMAGE_COMPOSE] Theorem
β’ βf g s. IMAGE (f β g) s = IMAGE f (IMAGE g s)
[IMAGE_CONG] Theorem
β’ βf s f' s'.
s = s' β§ (βx. x β s' β f x = f' x) β IMAGE f s = IMAGE f' s'
[IMAGE_CONST] Theorem
β’ βs c. IMAGE (Ξ»x. c) s = if s = β
then β
else {c}
[IMAGE_DELETE] Theorem
β’ βf x s. x β s β IMAGE f (s DELETE x) = IMAGE f s
[IMAGE_EMPTY] Theorem
β’ βf. IMAGE f β
= β
[IMAGE_EQ_EMPTY] Theorem
β’ βs f. (IMAGE f s = β
β s = β
) β§ (β
= IMAGE f s β s = β
)
[IMAGE_EQ_SING] Theorem
β’ IMAGE f s = {z} β s β β
β§ βx. x β s β f x = z
[IMAGE_FINITE] Theorem
β’ βs. FINITE s β βf. FINITE (IMAGE f s)
[IMAGE_FST_CROSS] Theorem
β’ βs t. t β β
β IMAGE FST (s Γ t) = s
[IMAGE_I] Theorem
β’ IMAGE I s = s
[IMAGE_ID] Theorem
β’ βs. IMAGE (Ξ»x. x) s = s
[IMAGE_II] Theorem
β’ IMAGE I = I
[IMAGE_IMAGE] Theorem
β’ βf g s. IMAGE f (IMAGE g s) = IMAGE (f β g) s
[IMAGE_IMAGE_partition] Theorem
β’ βR f s t.
INJ f s t β
IMAGE (IMAGE f) (partition R s) =
partition (inv_image R (LINV f s)) (IMAGE f s)
[IMAGE_IN] Theorem
β’ βx s. x β s β βf. f x β IMAGE f s
[IMAGE_INSERT] Theorem
β’ βf x s. IMAGE f (x INSERT s) = f x INSERT IMAGE f s
[IMAGE_INTER] Theorem
β’ βf s t. IMAGE f (s β© t) β IMAGE f s β© IMAGE f t
[IMAGE_PREIMAGE] Theorem
β’ βf s. IMAGE f (PREIMAGE f s) β s
[IMAGE_RESTRICTION] Theorem
β’ βf s t. s β t β IMAGE (RESTRICTION t f) s = IMAGE f s
[IMAGE_SING] Theorem
β’ βf x. IMAGE f {x} = {f x}
[IMAGE_SND_CROSS] Theorem
β’ βs t. s β β
β IMAGE SND (s Γ t) = t
[IMAGE_SUBSET] Theorem
β’ βs t. s β t β βf. IMAGE f s β IMAGE f t
[IMAGE_SUBSET_gen] Theorem
β’ βf s u t. s β u β§ IMAGE f u β t β IMAGE f s β t
[IMAGE_SURJ] Theorem
β’ βf s t. SURJ f s t β IMAGE f s = t
[IMAGE_UNION] Theorem
β’ βf s t. IMAGE f (s βͺ t) = IMAGE f s βͺ IMAGE f t
[IMAGE_applied] Theorem
β’ βy s f. IMAGE f s y β βx. y = f x β§ x β s
[IMAGE_o] Theorem
β’ βf g s. IMAGE (f β g) s = IMAGE f (IMAGE g s)
[INFINITE_DIFF_FINITE] Theorem
β’ βs t. INFINITE s β§ FINITE t β s DIFF t β β
[INFINITE_DIFF_FINITE'] Theorem
β’ βs t. INFINITE s β§ FINITE t β INFINITE (s DIFF t)
[INFINITE_EXPLICIT_ENUMERATE] Theorem
β’ βs. INFINITE s β INJ (Ξ»n. CHOICE (FUNPOW REST n s)) π(:num) s
[INFINITE_INHAB] Theorem
β’ βP. INFINITE P β βx. x β P
[INFINITE_INJ] Theorem
β’ βf s t. INJ f s t β§ INFINITE s β INFINITE t
[INFINITE_INJ_NOT_SURJ] Theorem
β’ βs. INFINITE s β βf. INJ f s s β§ Β¬SURJ f s s
[INFINITE_NUM_UNIV] Theorem
β’ INFINITE π(:num)
[INFINITE_PAIR_UNIV] Theorem
β’ FINITE π(:Ξ± # Ξ²) β FINITE π(:Ξ±) β§ FINITE π(:Ξ²)
[INFINITE_SUBSET] Theorem
β’ βs. INFINITE s β βt. s β t β INFINITE t
[INFINITE_UNIV] Theorem
β’ INFINITE π(:Ξ±) β βf. (βx y. f x = f y β x = y) β§ βy. βx. f x β y
[INJECTIVE_IMAGE_FINITE] Theorem
β’ βf. (βx y. f x = f y β x = y) β βs. FINITE (IMAGE f s) β FINITE s
[INJ_BIJ_SUBSET] Theorem
β’ s0 β s β§ INJ f s t β BIJ f s0 (IMAGE f s0)
[INJ_CARD] Theorem
β’ βf s t. INJ f s t β§ FINITE t β CARD s β€ CARD t
[INJ_CARD_IMAGE] Theorem
β’ βs. FINITE s β INJ f s t β CARD (IMAGE f s) = CARD s
[INJ_CARD_IMAGE_EQ] Theorem
β’ INJ f s t β FINITE s β CARD (IMAGE f s) = CARD s
[INJ_COMPOSE] Theorem
β’ βf g s t u. INJ f s t β§ INJ g t u β INJ (g β f) s u
[INJ_CONG] Theorem
β’ βf g s t. (βx. x β s β f x = g x) β (INJ f s t β INJ g s t)
[INJ_DELETE] Theorem
β’ βf s t. INJ f s t β βe. e β s β INJ f (s DELETE e) (t DELETE f e)
[INJ_ELEMENT] Theorem
β’ βf s t x. INJ f s t β§ x β s β f x β t
[INJ_EMPTY] Theorem
β’ βf. (βs. INJ f β
s) β§ βs. INJ f s β
β s = β
[INJ_EQ_11] Theorem
β’ βf s x y. INJ f s s β§ x β s β§ y β s β (f x = f y β x = y)
[INJ_EXTEND] Theorem
β’ βb s t x y.
INJ b s t β§ x β s β§ y β t β
INJ bβ¦x β¦ yβ¦ (x INSERT s) (y INSERT t)
[INJ_I] Theorem
β’ βs. INJ I s π(:Ξ±)
[INJ_ID] Theorem
β’ βs. INJ (Ξ»x. x) s s
[INJ_IFF] Theorem
β’ INJ f s t β
(βx. x β s β f x β t) β§ βx y. x β s β§ y β s β (f x = f y β x = y)
[INJ_IMAGE] Theorem
β’ βf s t. INJ f s t β INJ f s (IMAGE f s)
[INJ_IMAGE_BIJ] Theorem
β’ βs f. (βt. INJ f s t) β BIJ f s (IMAGE f s)
[INJ_IMAGE_DISJOINT] Theorem
β’ βP f.
INJ f P π(:Ξ²) β
βs t.
s β P β§ t β P β
(DISJOINT s t β DISJOINT (IMAGE f s) (IMAGE f t))
[INJ_IMAGE_EQ] Theorem
β’ βP f.
INJ f P π(:Ξ²) β
βs t. s β P β§ t β P β (IMAGE f s = IMAGE f t β s = t)
[INJ_IMAGE_INTER] Theorem
β’ βP f.
INJ f P π(:Ξ²) β
βs t. s β P β§ t β P β IMAGE f (s β© t) = IMAGE f s β© IMAGE f t
[INJ_IMAGE_SUBSET] Theorem
β’ βf s t. INJ f s t β IMAGE f s β t
[INJ_IMAGE_equiv_class] Theorem
β’ βf s t x.
INJ f s t β§ x β s β
IMAGE f (equiv_class R s x) =
equiv_class (inv_image R (LINV f s)) (IMAGE f s) (f x)
[INJ_IMP_11] Theorem
β’ βf. INJ f π(:Ξ±) π(:Ξ²) β βx y. f x = f y β x = y
[INJ_INL] Theorem
β’ (βx. x β s β INL x β t) β INJ INL s t
[INJ_INR] Theorem
β’ (βx. x β s β INR x β t) β INJ INR s t
[INJ_INSERT] Theorem
β’ βf x s t.
INJ f (x INSERT s) t β
INJ f s t β§ f x β t β§ βy. y β s β§ f x = f y β x = y
[INJ_I_IMAGE] Theorem
β’ βs f. INJ I (IMAGE f s) π(:Ξ²)
[INJ_LINV_OPT] Theorem
β’ INJ f s t β βx y. LINV_OPT f s y = SOME x β y = f x β§ x β s β§ y β t
[INJ_LINV_OPT_IMAGE] Theorem
β’ INJ (LINV_OPT f s) (IMAGE f s) (IMAGE SOME s)
[INJ_SUBSET] Theorem
β’ βf s t s0 t0. INJ f s t β§ s0 β s β§ t β t0 β INJ f s0 t0
[INJ_SUBSET_UNIV] Theorem
β’ βf s. INJ f π(:Ξ±) π(:Ξ²) β INJ f s π(:Ξ²)
[INSERT_COMM] Theorem
β’ βx y s. x INSERT y INSERT s = y INSERT x INSERT s
[INSERT_DELETE] Theorem
β’ βx s. x β s β x INSERT s DELETE x = s
[INSERT_DIFF] Theorem
β’ βs t x.
(x INSERT s) DIFF t =
if x β t then s DIFF t else x INSERT s DIFF t
[INSERT_EQ_SING] Theorem
β’ βs x y. x INSERT s = {y} β x = y β§ s β {y}
[INSERT_INSERT] Theorem
β’ βx s. x INSERT x INSERT s = x INSERT s
[INSERT_INTER] Theorem
β’ βx s t. (x INSERT s) β© t = if x β t then x INSERT s β© t else s β© t
[INSERT_SING_UNION] Theorem
β’ βs x. x INSERT s = {x} βͺ s
[INSERT_SUBSET] Theorem
β’ βx s t. x INSERT s β t β x β t β§ s β t
[INSERT_UNION] Theorem
β’ βx s t. (x INSERT s) βͺ t = if x β t then s βͺ t else x INSERT s βͺ t
[INSERT_UNION_EQ] Theorem
β’ βx s t. (x INSERT s) βͺ t = x INSERT s βͺ t
[INSERT_UNIV] Theorem
β’ βx. x INSERT π(:Ξ±) = π(:Ξ±)
[INSERT_applied] Theorem
β’ βx y s. (y INSERT s) x β x = y β¨ x β s
[INTER_ASSOC] Theorem
β’ βs t u. s β© (t β© u) = s β© t β© u
[INTER_BIGUNION] Theorem
β’ (βs t. BIGUNION s β© t = BIGUNION {x β© t | x β s}) β§
βs t. t β© BIGUNION s = BIGUNION {t β© x | x β s}
[INTER_COMM] Theorem
β’ βs t. s β© t = t β© s
[INTER_CROSS] Theorem
β’ βA B C D. A Γ B β© C Γ D = (A β© C) Γ (B β© D)
[INTER_EMPTY] Theorem
β’ (βs. β
β© s = β
) β§ βs. s β© β
= β
[INTER_FINITE] Theorem
β’ βs. FINITE s β βt. FINITE (s β© t)
[INTER_IDEMPOT] Theorem
β’ βs. s β© s = s
[INTER_OVER_UNION] Theorem
β’ βs t u. s βͺ t β© u = (s βͺ t) β© (s βͺ u)
[INTER_SING] Theorem
β’ βs x. x β s β s β© {x} = {x}
[INTER_SUBSET] Theorem
β’ (βs t. s β© t β s) β§ βs t. t β© s β s
[INTER_SUBSET_EQN] Theorem
β’ (A β© B = A β A β B) β§ (A β© B = B β B β A)
[INTER_UNION] Theorem
β’ (A βͺ B) β© A = A β§ (B βͺ A) β© A = A β§ A β© (A βͺ B) = A β§
A β© (B βͺ A) = A
[INTER_UNION_COMPL] Theorem
β’ βs t. s β© t = COMPL (COMPL s βͺ COMPL t)
[INTER_UNIV] Theorem
β’ (βs. π(:Ξ±) β© s = s) β§ βs. s β© π(:Ξ±) = s
[INTER_applied] Theorem
β’ βs t x. (s β© t) x β x β s β§ x β t
[IN_ABS] Theorem
β’ βx P. x β (Ξ»x. P x) β P x
[IN_APP] Theorem
β’ βx P. x β P β P x
[IN_BIGINTER] Theorem
β’ x β BIGINTER B β βP. P β B β x β P
[IN_BIGINTER_IMAGE] Theorem
β’ βx f s. x β BIGINTER (IMAGE f s) β βy. y β s β x β f y
[IN_BIGUNION] Theorem
β’ βx sos. x β BIGUNION sos β βs. x β s β§ s β sos
[IN_BIGUNION_IMAGE] Theorem
β’ βf s y. y β BIGUNION (IMAGE f s) β βx. x β s β§ y β f x
[IN_COMPL] Theorem
β’ βx s. x β COMPL s β x β s
[IN_COUNT] Theorem
β’ βm n. m β count n β m < n
[IN_CROSS] Theorem
β’ βP Q x. x β P Γ Q β FST x β P β§ SND x β Q
[IN_DELETE] Theorem
β’ βs x y. x β s DELETE y β x β s β§ x β y
[IN_DELETE_EQ] Theorem
β’ βs x x'. (x β s β x' β s) β (x β s DELETE x' β x' β s DELETE x)
[IN_DFUNSET] Theorem
β’ βf P Q. f β DFUNSET P Q β βx. x β P β f x β Q x
[IN_DIFF] Theorem
β’ βs t x. x β s DIFF t β x β s β§ x β t
[IN_DISJOINT] Theorem
β’ βs t. DISJOINT s t β Β¬βx. x β s β§ x β t
[IN_EQ_UNIV_IMP] Theorem
β’ βs. s = π(:Ξ±) β βv. v β s
[IN_FUNSET] Theorem
β’ βf P Q. f β FUNSET P Q β βx. x β P β f x β Q
[IN_GSPEC] Theorem
β’ βy x P. P y β§ x = f y β x β {f x | P x}
[IN_GSPEC_IFF] Theorem
β’ y β {x | P x} β P y
[IN_IMAGE] Theorem
β’ βy s f. y β IMAGE f s β βx. y = f x β§ x β s
[IN_INFINITE_NOT_FINITE] Theorem
β’ βs t. INFINITE s β§ FINITE t β βx. x β s β§ x β t
[IN_INSERT] Theorem
β’ βx y s. x β y INSERT s β x = y β¨ x β s
[IN_INSERT_EXPAND] Theorem
β’ βx y P. x β y INSERT P β x = y β¨ x β y β§ x β P
[IN_INTER] Theorem
β’ βs t x. x β s β© t β x β s β§ x β t
[IN_POW] Theorem
β’ βset e. e β POW set β e β set
[IN_PREIMAGE] Theorem
β’ βf s x. x β PREIMAGE f s β f x β s
[IN_REST] Theorem
β’ βx s. x β REST s β x β s β§ x β CHOICE s
[IN_SING] Theorem
β’ βx y. x β {y} β x = y
[IN_UNION] Theorem
β’ βs t x. x β s βͺ t β x β s β¨ x β t
[IN_UNIV] Theorem
β’ βx. x β π(:Ξ±)
[IN_disjUNION] Theorem
β’ (INL a β A β B β a β A) β§ (INR b β A β B β b β B)
[ITSET_CONG] Theorem
β’ βf g. f = g β ITSET f = ITSET g
[ITSET_EMPTY] Theorem
β’ βf b. ITSET f β
b = b
[ITSET_IND] Theorem
β’ βP. (βs b. (FINITE s β§ s β β
β P (REST s) (f (CHOICE s) b)) β P s b) β
βv v1. P v v1
[ITSET_INSERT] Theorem
β’ βs. FINITE s β
βf x b.
ITSET f (x INSERT s) b =
ITSET f (REST (x INSERT s)) (f (CHOICE (x INSERT s)) b)
[ITSET_PROPERTY] Theorem
β’ βs f b.
FINITE s β§ s β β
β
ITSET f s b = ITSET f (REST s) (f (CHOICE s) b)
[ITSET_REDUCTION] Theorem
β’ βf. (βx y z. f x (f y z) = f y (f x z)) β
βs x b.
FINITE s β§ x β s β ITSET f (x INSERT s) b = f x (ITSET f s b)
[ITSET_SING] Theorem
β’ βf x a. ITSET f {x} a = f x a
[ITSET_THM] Theorem
β’ βs f b.
FINITE s β
ITSET f s b =
if s = β
then b else ITSET f (REST s) (f (CHOICE s) b)
[ITSET_def] Theorem
β’ βs f b.
ITSET f s b =
if FINITE s then
if s = β
then b else ITSET f (REST s) (f (CHOICE s) b)
else ARB
[K_SUBSET] Theorem
β’ βx y. K x β y β Β¬x β¨ π(:Ξ±) β y
[KoenigsLemma] Theorem
β’ βR. (βx. FINITE {y | R x y}) β
βx. INFINITE {y | Rκ³ x y} β
βf. f 0 = x β§ βn. R (f n) (f (SUC n))
[KoenigsLemma_WF] Theorem
β’ βR. (βx. FINITE {y | R x y}) β§ WF Rα΅ β βx. FINITE {y | Rκ³ x y}
[LESS_CARD_DIFF] Theorem
β’ βt. FINITE t β βs. FINITE s β CARD t < CARD s β 0 < CARD (s DIFF t)
[LINV_DEF] Theorem
β’ βf s t. INJ f s t β βx. x β s β LINV f s (f x) = x
[LINV_OPT_THM] Theorem
β’ LINV_OPT f s y = SOME x β x β s β§ f x = y
[MAX_SET_ELIM] Theorem
β’ βP Q.
FINITE P β§ (P = β
β Q 0) β§
(βx. (βy. y β P β y β€ x) β§ x β P β Q x) β
Q (MAX_SET P)
[MAX_SET_EMPTY] Theorem
β’ MAX_SET β
= 0
[MAX_SET_EQ_0] Theorem
β’ βs. FINITE s β (MAX_SET s = 0 β s = β
β¨ s = {0})
[MAX_SET_INTER] Theorem
β’ βA B.
FINITE A β§ FINITE B β
MAX_SET (A β© B) β€ MIN (MAX_SET A) (MAX_SET B)
[MAX_SET_IN_SET] Theorem
β’ βs. FINITE s β§ s β β
β MAX_SET s β s
[MAX_SET_LESS] Theorem
β’ βs n. FINITE s β§ MAX_SET s < n β βx. x β s β x < n
[MAX_SET_PROPERTY] Theorem
β’ βs. FINITE s β βx. x β s β x β€ MAX_SET s
[MAX_SET_REWRITES] Theorem
β’ MAX_SET β
= 0 β§ MAX_SET {e} = e
[MAX_SET_SING] Theorem
β’ βe. MAX_SET {e} = e
[MAX_SET_TEST] Theorem
β’ βs. FINITE s β§ s β β
β
βx. x β s β§ (βy. y β s β y β€ x) β x = MAX_SET s
[MAX_SET_TEST_IFF] Theorem
β’ βs. FINITE s β§ s β β
β
βx. x β s β (MAX_SET s = x β βy. y β s β y β€ x)
[MAX_SET_THM] Theorem
β’ MAX_SET β
= 0 β§
βe s. FINITE s β MAX_SET (e INSERT s) = MAX e (MAX_SET s)
[MAX_SET_UNION] Theorem
β’ βA B.
FINITE A β§ FINITE B β
MAX_SET (A βͺ B) = MAX (MAX_SET A) (MAX_SET B)
[MEMBER_NOT_EMPTY] Theorem
β’ βs. (βx. x β s) β s β β
[MIN_SET_ELIM] Theorem
β’ βP Q.
P β β
β§ (βx. (βy. y β P β x β€ y) β§ x β P β Q x) β Q (MIN_SET P)
[MIN_SET_EQ_0] Theorem
β’ βs. s β β
β (MIN_SET s = 0 β 0 β s)
[MIN_SET_IN_SET] Theorem
β’ βs. s β β
β MIN_SET s β s
[MIN_SET_LEM] Theorem
β’ βs. s β β
β MIN_SET s β s β§ βx. x β s β MIN_SET s β€ x
[MIN_SET_LEQ_MAX_SET] Theorem
β’ βs. s β β
β§ FINITE s β MIN_SET s β€ MAX_SET s
[MIN_SET_PROPERTY] Theorem
β’ βs. s β β
β βx. x β s β MIN_SET s β€ x
[MIN_SET_SING] Theorem
β’ βe. MIN_SET {e} = e
[MIN_SET_TEST] Theorem
β’ βs. s β β
β βx. x β s β§ (βy. y β s β x β€ y) β x = MIN_SET s
[MIN_SET_TEST_IFF] Theorem
β’ βs. s β β
β βx. x β s β (MIN_SET s = x β βy. y β s β x β€ y)
[MIN_SET_THM] Theorem
β’ (βe. MIN_SET {e} = e) β§
βs e1 e2.
MIN_SET (e1 INSERT e2 INSERT s) = MIN e1 (MIN_SET (e2 INSERT s))
[MIN_SET_THM'] Theorem
β’ (βe. MIN_SET {e} = e) β§
βe s. s β β
β MIN_SET (e INSERT s) = MIN e (MIN_SET s)
[MIN_SET_UNION] Theorem
β’ βA B.
FINITE A β§ FINITE B β§ A β β
β§ B β β
β
MIN_SET (A βͺ B) = MIN (MIN_SET A) (MIN_SET B)
[NOT_EMPTY_INSERT] Theorem
β’ βx s. β
β x INSERT s
[NOT_EMPTY_SING] Theorem
β’ βx. β
β {x}
[NOT_EQUAL_SETS] Theorem
β’ βs t. s β t β βx. x β t β x β s
[NOT_INSERT_EMPTY] Theorem
β’ βx s. x INSERT s β β
[NOT_IN_EMPTY] Theorem
β’ βx. x β β
[NOT_IN_FINITE] Theorem
β’ INFINITE π(:Ξ±) β βs. FINITE s β βx. x β s
[NOT_PSUBSET_EMPTY] Theorem
β’ βs. Β¬(s β β
)
[NOT_SING_EMPTY] Theorem
β’ βx. {x} β β
[NOT_UNIV_PSUBSET] Theorem
β’ βs. Β¬(π(:Ξ±) β s)
[NUM_2D_BIJ] Theorem
β’ βf. BIJ f (π(:num) Γ π(:num)) π(:num)
[NUM_2D_BIJ_BIG_SQUARE] Theorem
β’ βf N.
BIJ f π(:num) (π(:num) Γ π(:num)) β
βk. IMAGE f (count N) β count k Γ count k
[NUM_2D_BIJ_INV] Theorem
β’ βf. BIJ f π(:num) (π(:num) Γ π(:num))
[NUM_2D_BIJ_NZ] Theorem
β’ βf. BIJ f (π(:num) Γ (π(:num) DIFF {0})) π(:num)
[NUM_2D_BIJ_NZ_ALT] Theorem
β’ βf. BIJ f (π(:num) Γ π(:num)) (π(:num) DIFF {0})
[NUM_2D_BIJ_NZ_ALT2] Theorem
β’ βf. BIJ f ((π(:num) DIFF {0}) Γ (π(:num) DIFF {0})) π(:num)
[NUM_2D_BIJ_NZ_ALT2_INV] Theorem
β’ βf. BIJ f π(:num) ((π(:num) DIFF {0}) Γ (π(:num) DIFF {0}))
[NUM_2D_BIJ_NZ_ALT_INV] Theorem
β’ βf. BIJ f (π(:num) DIFF {0}) (π(:num) Γ π(:num))
[NUM_2D_BIJ_NZ_INV] Theorem
β’ βf. BIJ f π(:num) (π(:num) Γ (π(:num) DIFF {0}))
[NUM_2D_BIJ_SMALL_SQUARE] Theorem
β’ βf k.
BIJ f π(:num) (π(:num) Γ π(:num)) β
βN. count k Γ count k β IMAGE f (count N)
[NUM_SET_WOP] Theorem
β’ βs. (βn. n β s) β βn. n β s β§ βm. m β s β n β€ m
[ONE_ELEMENT_SING] Theorem
β’ βs a. s β β
β§ (βk. k β s β k = a) β s = {a}
[PAIR_IN_GSPEC_1] Theorem
β’ (a,b) β {(y,x) | P y} β P a β§ b = x
[PAIR_IN_GSPEC_2] Theorem
β’ (a,b) β {(x,y) | P y} β P b β§ a = x
[PAIR_IN_GSPEC_IFF] Theorem
β’ (x,y) β {(x,y) | P x y} β P x y
[PAIR_IN_GSPEC_same] Theorem
β’ (a,b) β {(x,x) | P x} β P a β§ a = b
[PHP] Theorem
β’ βf s t. FINITE t β§ CARD t < CARD s β Β¬INJ f s t
[PI_CONSTANT] Theorem
β’ βs. FINITE s β βf k. (βx. x β s β f x = k) β Ξ f s = k ** CARD s
[POW_EMPTY] Theorem
β’ βs. POW s β β
[POW_EQNS] Theorem
β’ POW β
= {β
} β§
βe s.
POW (e INSERT s) = (let ps = POW s in IMAGE ($INSERT e) ps βͺ ps)
[POW_INSERT] Theorem
β’ βe s. POW (e INSERT s) = IMAGE ($INSERT e) (POW s) βͺ POW s
[POW_applied] Theorem
β’ βset e. POW set e β e β set
[PREIMAGE_ALT] Theorem
β’ βf s. PREIMAGE f s = s β f
[PREIMAGE_BIGUNION] Theorem
β’ βf s. PREIMAGE f (BIGUNION s) = BIGUNION (IMAGE (PREIMAGE f) s)
[PREIMAGE_COMP] Theorem
β’ βf g s. PREIMAGE f (PREIMAGE g s) = PREIMAGE (g β f) s
[PREIMAGE_COMPL] Theorem
β’ βf s. PREIMAGE f (COMPL s) = COMPL (PREIMAGE f s)
[PREIMAGE_COMPL_INTER] Theorem
β’ βf t sp. PREIMAGE f (COMPL t) β© sp = sp DIFF PREIMAGE f t
[PREIMAGE_CROSS] Theorem
β’ βf a b.
PREIMAGE f (a Γ b) = PREIMAGE (FST β f) a β© PREIMAGE (SND β f) b
[PREIMAGE_DIFF] Theorem
β’ βf s t. PREIMAGE f (s DIFF t) = PREIMAGE f s DIFF PREIMAGE f t
[PREIMAGE_DISJOINT] Theorem
β’ βf s t. DISJOINT s t β DISJOINT (PREIMAGE f s) (PREIMAGE f t)
[PREIMAGE_EMPTY] Theorem
β’ βf. PREIMAGE f β
= β
[PREIMAGE_I] Theorem
β’ PREIMAGE I = I β§ PREIMAGE (Ξ»x. x) = (Ξ»x. x)
[PREIMAGE_IMAGE] Theorem
β’ βf s. s β PREIMAGE f (IMAGE f s)
[PREIMAGE_INTER] Theorem
β’ βf s t. PREIMAGE f (s β© t) = PREIMAGE f s β© PREIMAGE f t
[PREIMAGE_K] Theorem
β’ βx s. PREIMAGE (K x) s = if x β s then π(:Ξ²) else β
[PREIMAGE_SUBSET] Theorem
β’ βf s t. s β t β PREIMAGE f s β PREIMAGE f t
[PREIMAGE_UNION] Theorem
β’ βf s t. PREIMAGE f (s βͺ t) = PREIMAGE f s βͺ PREIMAGE f t
[PREIMAGE_UNIV] Theorem
β’ βf. PREIMAGE f π(:Ξ²) = π(:Ξ±)
[PREIMAGE_applied] Theorem
β’ βf s x. PREIMAGE f s x β f x β s
[PREIMAGE_o] Theorem
β’ βf g s. PREIMAGE (f β g) s = PREIMAGE g (s β f)
[PROD_IMAGE_CONG] Theorem
β’ βs f1 f2. (βx. x β s β f1 x = f2 x) β Ξ f1 s = Ξ f2 s
[PROD_IMAGE_CONSTANT] Theorem
β’ βs. FINITE s β βc. Ξ (K c) s = c ** CARD s
[PROD_IMAGE_DELETE] Theorem
β’ βs. FINITE s β
βf e.
0 < f e β
Ξ f (s DELETE e) = if e β s then Ξ f s DIV f e else Ξ f s
[PROD_IMAGE_EMPTY] Theorem
β’ βf. Ξ f β
= 1
[PROD_IMAGE_EQ_0] Theorem
β’ βs. FINITE s β (Ξ f s = 0 β βx. x β s β§ f x = 0)
[PROD_IMAGE_EQ_1] Theorem
β’ βs. FINITE s β (Ξ f s = 1 β IMAGE f s β {1})
[PROD_IMAGE_INSERT] Theorem
β’ βs. FINITE s β βf e. e β s β Ξ f (e INSERT s) = f e * Ξ f s
[PROD_IMAGE_THM] Theorem
β’ βf. Ξ f β
= 1 β§
βe s. FINITE s β Ξ f (e INSERT s) = f e * Ξ f (s DELETE e)
[PROD_SET_EMPTY] Theorem
β’ PROD_SET β
= 1
[PROD_SET_IMAGE_REDUCTION] Theorem
β’ βf s x.
FINITE (IMAGE f s) β§ f x β IMAGE f s β
PROD_SET (IMAGE f (x INSERT s)) = f x * PROD_SET (IMAGE f s)
[PROD_SET_INSERT] Theorem
β’ βx s. FINITE s β§ x β s β PROD_SET (x INSERT s) = x * PROD_SET s
[PROD_SET_THM] Theorem
β’ PROD_SET β
= 1 β§
βx s. FINITE s β PROD_SET (x INSERT s) = x * PROD_SET (s DELETE x)
[PSUBSET_EQN] Theorem
β’ βs1 s2. s1 β s2 β s1 β s2 β§ Β¬(s2 β s1)
[PSUBSET_FINITE] Theorem
β’ βs. FINITE s β βt. t β s β FINITE t
[PSUBSET_INSERT_SUBSET] Theorem
β’ βs t. s β t β βx. x β s β§ x INSERT s β t
[PSUBSET_IRREFL] Theorem
β’ βs. Β¬(s β s)
[PSUBSET_MEMBER] Theorem
β’ βs t. s β t β s β t β§ βy. y β t β§ y β s
[PSUBSET_SING] Theorem
β’ βs x. x β {s} β x = β
[PSUBSET_SUBSET_TRANS] Theorem
β’ βs t u. s β t β§ t β u β s β u
[PSUBSET_TRANS] Theorem
β’ βs t u. s β t β§ t β u β s β u
[PSUBSET_UNIV] Theorem
β’ βs. s β π(:Ξ±) β βx. x β s
[RC_PSUBSET] Theorem
β’ RC $PSUBSET = $SUBSET
[RC_SUBSET_THM] Theorem
β’ RC $SUBSET = $SUBSET
[REL_RESTRICT_EMPTY] Theorem
β’ REL_RESTRICT R β
= β
α΅£
[REL_RESTRICT_SUBSET] Theorem
β’ s1 β s2 β REL_RESTRICT R s1 βα΅£ REL_RESTRICT R s2
[RESTRICTION_COMPOSE] Theorem
β’ βf g s t.
IMAGE f s β t β
RESTRICTION s (RESTRICTION t g β RESTRICTION s f) =
RESTRICTION s (g β f)
[RESTRICTION_COMPOSE_LEFT] Theorem
β’ βf g s t.
IMAGE f s β t β
RESTRICTION s (RESTRICTION t g β f) = RESTRICTION s (g β f)
[RESTRICTION_COMPOSE_RIGHT] Theorem
β’ βf g s. RESTRICTION s (g β RESTRICTION s f) = RESTRICTION s (g β f)
[RESTRICTION_EXTENSION] Theorem
β’ βs f g. RESTRICTION s f = RESTRICTION s g β βx. x β s β f x = g x
[RESTRICTION_FIXPOINT] Theorem
β’ βs f. RESTRICTION s f = f β f β EXTENSIONAL s
[RESTRICTION_IDEMP] Theorem
β’ βs f. RESTRICTION s (RESTRICTION s f) = RESTRICTION s f
[RESTRICTION_IN_EXTENSIONAL] Theorem
β’ βs f. RESTRICTION s f β EXTENSIONAL s
[RESTRICTION_RESTRICTION] Theorem
β’ βs t f. s β t β RESTRICTION s (RESTRICTION t f) = RESTRICTION s f
[RESTRICTION_UNIQUE] Theorem
β’ βs f g.
RESTRICTION s f = g β EXTENSIONAL s g β§ βx. x β s β f x = g x
[RESTRICTION_UNIQUE_ALT] Theorem
β’ βs f g.
f = RESTRICTION s g β EXTENSIONAL s f β§ βx. x β s β f x = g x
[REST_PSUBSET] Theorem
β’ βs. s β β
β REST s β s
[REST_SING] Theorem
β’ βx. REST {x} = β
[REST_SUBSET] Theorem
β’ βs. REST s β s
[REST_applied] Theorem
β’ βx s. REST s x β x β s β§ x β CHOICE s
[RINV_DEF] Theorem
β’ βf s t. SURJ f s t β βx. x β t β f (RINV f s x) = x
[RTC_PSUBSET] Theorem
β’ $PSUBSETκ³ = $SUBSET
[RTC_SUBSET_THM] Theorem
β’ $SUBSETκ³ = $SUBSET
[SCHROEDER_BERNSTEIN] Theorem
β’ βs t. (βf. INJ f s t) β§ (βg. INJ g t s) β βh. BIJ h s t
[SCHROEDER_BERNSTEIN_AUTO] Theorem
β’ βs t. t β s β§ (βf. INJ f s t) β βg. BIJ g s t
[SCHROEDER_CLOSE] Theorem
β’ βf s. x β schroeder_close f s β βn. x β FUNPOW (IMAGE f) n s
[SCHROEDER_CLOSED] Theorem
β’ βf s. IMAGE f (schroeder_close f s) β schroeder_close f s
[SCHROEDER_CLOSE_SET] Theorem
β’ βf s t. f β FUNSET s s β§ t β s β schroeder_close f t β s
[SCHROEDER_CLOSE_SUBSET] Theorem
β’ βf s. s β schroeder_close f s
[SET_CASES] Theorem
β’ βs. s = β
β¨ βx t. s = x INSERT t β§ x β t
[SET_EQ_SUBSET] Theorem
β’ βs t. s = t β s β t β§ t β s
[SET_MINIMUM] Theorem
β’ βs M. (βx. x β s) β βx. x β s β§ βy. y β s β M x β€ M y
[SIGMA_CARD_CONSTANT] Theorem
β’ βn s. FINITE s β§ (βe. e β s β CARD e = n) β β CARD s = n * CARD s
[SIGMA_CARD_SAME_SIZE_SETS] Theorem
β’ βn s. FINITE s β§ (βe. e β s β CARD e = n) β β CARD s = n * CARD s
[SIGMA_CONG] Theorem
β’ βs f1 f2. (βx. x β s β f1 x = f2 x) β β f1 s = β f2 s
[SIGMA_CONSTANT] Theorem
β’ βs. FINITE s β βf k. (βx. x β s β f x = k) β β f s = k * CARD s
[SIGMA_LE_SIGMA] Theorem
β’ βs. FINITE s β βf g. (βx. x β s β f x β€ g x) β β f s β€ β g s
[SIMPLE_FINITE_INDUCT] Theorem
β’ βP. P β
β§ (βs. P s β βe. P (e INSERT s)) β βs. FINITE s β P s
[SING] Theorem
β’ βx. SING {x}
[SING_CARD_1] Theorem
β’ βs. SING s β CARD s = 1
[SING_DELETE] Theorem
β’ βx. {x} DELETE x = β
[SING_ELEMENT] Theorem
β’ βs. SING s β βx y. x β s β§ y β s β x = y
[SING_EMPTY] Theorem
β’ SING β
β F
[SING_FINITE] Theorem
β’ βs. SING s β FINITE s
[SING_IFF_CARD1] Theorem
β’ βs. SING s β CARD s = 1 β§ FINITE s
[SING_IFF_EMPTY_REST] Theorem
β’ βs. SING s β s β β
β§ REST s = β
[SING_INSERT] Theorem
β’ SING (x INSERT s) β s = β
β¨ s = {x}
[SING_INTER] Theorem
β’ βs x. {x} β© s = if x β s then {x} else β
[SING_ONE_ELEMENT] Theorem
β’ βs. s β β
β (SING s β βx y. x β s β§ y β s β x = y)
[SING_TEST] Theorem
β’ βs. SING s β s β β
β§ βx y. x β s β§ y β s β x = y
[SING_UNION] Theorem
β’ SING (s βͺ t) β
SING s β§ t = β
β¨ SING t β§ s = β
β¨ SING s β§ SING t β§ s = t
[SING_applied] Theorem
β’ βx y. {y} x β x = y
[SING_partitions] Theorem
β’ βx w. {x} partitions w β x = w β§ w β β
[SPECIFICATION] Theorem
β’ βP x. x β P β P x
[SUBSET_ADD] Theorem
β’ βf n d. (βn. f n β f (SUC n)) β f n β f (n + d)
[SUBSET_ANTISYM] Theorem
β’ βs t. s β t β§ t β s β s = t
[SUBSET_ANTISYM_EQ] Theorem
β’ βs t. s β t β§ t β s β s = t
[SUBSET_BIGINTER] Theorem
β’ βX P. X β BIGINTER P β βY. Y β P β X β Y
[SUBSET_BIGUNION] Theorem
β’ βf g. f β g β BIGUNION f β BIGUNION g
[SUBSET_BIGUNION_I] Theorem
β’ βx P. x β P β x β BIGUNION P
[SUBSET_BIGUNION_SUBSET_I] Theorem
β’ B β A β§ A β As β B β BIGUNION As
[SUBSET_COMMUTING_ITSET_INSERT] Theorem
β’ βf s t.
FINITE s β§ s β t β§ closure_comm_assoc_fun f t β
βx b::t. ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b)
[SUBSET_COMMUTING_ITSET_RECURSES] Theorem
β’ βf s t.
FINITE s β§ s β t β§ closure_comm_assoc_fun f t β
βx b::t. ITSET f (x INSERT s) b = f x (ITSET f (s DELETE x) b)
[SUBSET_COMMUTING_ITSET_REDUCTION] Theorem
β’ βf s t.
FINITE s β§ s β t β§ closure_comm_assoc_fun f t β
βx b::t. ITSET f s (f x b) = f x (ITSET f s b)
[SUBSET_CROSS] Theorem
β’ βa b c d. a β b β§ c β d β a Γ c β b Γ d
[SUBSET_DELETE] Theorem
β’ βx s t. s β t DELETE x β x β s β§ s β t
[SUBSET_DELETE_BOTH] Theorem
β’ βs1 s2 x. s1 β s2 β s1 DELETE x β s2 DELETE x
[SUBSET_DIFF] Theorem
β’ βs1 s2 s3. s1 β s2 DIFF s3 β s1 β s2 β§ DISJOINT s1 s3
[SUBSET_DIFF_EMPTY] Theorem
β’ βs t. s DIFF t = β
β s β t
[SUBSET_DISJOINT] Theorem
β’ βs t u v. DISJOINT s t β§ u β s β§ v β t β DISJOINT u v
[SUBSET_EMPTY] Theorem
β’ βs. s β β
β s = β
[SUBSET_EQ_CARD] Theorem
β’ βs. FINITE s β βt. FINITE t β§ CARD s = CARD t β§ s β t β s = t
[SUBSET_FINITE] Theorem
β’ βs. FINITE s β βt. t β s β FINITE t
[SUBSET_FINITE_I] Theorem
β’ βs t. FINITE s β§ t β s β FINITE t
[SUBSET_IMAGE] Theorem
β’ βf s t. s β IMAGE f t β βu. u β t β§ s = IMAGE f u
[SUBSET_INSERT] Theorem
β’ βx s. x β s β βt. s β x INSERT t β s β t
[SUBSET_INSERT_DELETE] Theorem
β’ βx s t. s β x INSERT t β s DELETE x β t
[SUBSET_INSERT_RIGHT] Theorem
β’ βe s1 s2. s1 β s2 β s1 β e INSERT s2
[SUBSET_INTER] Theorem
β’ βs t u. s β t β© u β s β t β§ s β u
[SUBSET_INTER1] Theorem
β’ βs t. s β t β s β© t = s
[SUBSET_INTER2] Theorem
β’ βs t. s β t β t β© s = s
[SUBSET_INTER_ABSORPTION] Theorem
β’ βs t. s β t β s β© t = s
[SUBSET_K] Theorem
β’ βx y. x β K y β x β β
β¨ y
[SUBSET_MAX_SET] Theorem
β’ βI J. FINITE I β§ FINITE J β§ I β J β MAX_SET I β€ MAX_SET J
[SUBSET_MIN_SET] Theorem
β’ βI J. I β β
β§ J β β
β§ I β J β MIN_SET J β€ MIN_SET I
[SUBSET_OF_INSERT] Theorem
β’ βx s. s β x INSERT s
[SUBSET_POW] Theorem
β’ βs1 s2. s1 β s2 β POW s1 β POW s2
[SUBSET_PSUBSET_TRANS] Theorem
β’ βs t u. s β t β§ t β u β s β u
[SUBSET_REFL] Theorem
β’ βs. s β s
[SUBSET_SING] Theorem
β’ x β {a} β x = β
β¨ x = {a}
[SUBSET_THM] Theorem
β’ βP Q. P β Q β βx. x β P β x β Q
[SUBSET_TRANS] Theorem
β’ βs t u. s β t β§ t β u β s β u
[SUBSET_UNION] Theorem
β’ (βs t. s β s βͺ t) β§ βs t. s β t βͺ s
[SUBSET_UNION_ABSORPTION] Theorem
β’ βs t. s β t β s βͺ t = t
[SUBSET_UNIV] Theorem
β’ βs. s β π(:Ξ±)
[SUBSET_applied] Theorem
β’ βs t. s β t β βx. s x β t x
[SUBSET_count_MAX_SET] Theorem
β’ FINITE s β s β count (MAX_SET s + 1)
[SUBSET_reflexive] Theorem
β’ reflexive $SUBSET
[SUBSET_transitive] Theorem
β’ transitive $SUBSET
[SUM_IMAGE_ADD] Theorem
β’ βs. FINITE s β β (Ξ»x. f x + g x) s = β f s + β g s
[SUM_IMAGE_CONG] Theorem
β’ s1 = s2 β§ (βx. x β s2 β f1 x = f2 x) β β f1 s1 = β f2 s2
[SUM_IMAGE_CONSTANT] Theorem
β’ βs. FINITE s β βc. β (K c) s = c * CARD s
[SUM_IMAGE_DELETE] Theorem
β’ βf s.
FINITE s β
βe. β f (s DELETE e) = if e β s then β f s β f e else β f s
[SUM_IMAGE_DISJOINT] Theorem
β’ βs t.
FINITE s β§ FINITE t β§ DISJOINT s t β
βf. β f (s βͺ t) = β f s + β f t
[SUM_IMAGE_EMPTY] Theorem
β’ βf. β f β
= 0
[SUM_IMAGE_INJ_o] Theorem
β’ βs. FINITE s β
βg. INJ g s π(:Ξ±) β βf. β f (IMAGE g s) = β (f β g) s
[SUM_IMAGE_INSERT] Theorem
β’ βf s. FINITE s β βe. e β s β β f (e INSERT s) = f e + β f s
[SUM_IMAGE_IN_LE] Theorem
β’ βf s e. FINITE s β§ e β s β f e β€ β f s
[SUM_IMAGE_MONO_LESS] Theorem
β’ βs. FINITE s β
(βx. x β s β§ f x < g x) β§ (βx. x β s β f x β€ g x) β
β f s < β g s
[SUM_IMAGE_MONO_LESS_EQ] Theorem
β’ βs. FINITE s β (βx. x β s β f x β€ g x) β β f s β€ β g s
[SUM_IMAGE_MONO_LT] Theorem
β’ βs. FINITE s β§ s β β
β
βf g. (βx. x β s β f x < g x) β β f s < β g s
[SUM_IMAGE_PERMUTES] Theorem
β’ βs. FINITE s β βg. g PERMUTES s β βf. β (f β g) s = β f s
[SUM_IMAGE_SING] Theorem
β’ βf e. β f {e} = f e
[SUM_IMAGE_SUBSET_LE] Theorem
β’ βf s t. FINITE s β§ t β s β β f t β€ β f s
[SUM_IMAGE_THM] Theorem
β’ βf. β f β
= 0 β§
βe s. FINITE s β β f (e INSERT s) = f e + β f (s DELETE e)
[SUM_IMAGE_UNION] Theorem
β’ βf s t.
FINITE s β§ FINITE t β β f (s βͺ t) = β f s + β f t β β f (s β© t)
[SUM_IMAGE_UNION_EQN] Theorem
β’ βs t.
FINITE s β§ FINITE t β
βf. β f (s βͺ t) + β f (s β© t) = β f s + β f t
[SUM_IMAGE_ZERO] Theorem
β’ βs. FINITE s β (β f s = 0 β βx. x β s β f x = 0)
[SUM_IMAGE_lower_bound] Theorem
β’ βs. FINITE s β βn. (βx. x β s β n β€ f x) β CARD s * n β€ β f s
[SUM_IMAGE_upper_bound] Theorem
β’ βs. FINITE s β βn. (βx. x β s β f x β€ n) β β f s β€ CARD s * n
[SUM_SAME_IMAGE] Theorem
β’ βP. FINITE P β
βf p. p β P β§ (βq. q β P β f p = f q) β β f P = CARD P * f p
[SUM_SET_DELETE] Theorem
β’ βs. FINITE s β
βe. SUM_SET (s DELETE e) =
if e β s then SUM_SET s β e else SUM_SET s
[SUM_SET_EMPTY] Theorem
β’ SUM_SET β
= 0
[SUM_SET_INSERT] Theorem
β’ βs x. FINITE s β§ x β s β SUM_SET (x INSERT s) = x + SUM_SET s
[SUM_SET_IN_LE] Theorem
β’ βx s. FINITE s β§ x β s β x β€ SUM_SET s
[SUM_SET_SING] Theorem
β’ βn. SUM_SET {n} = n
[SUM_SET_SUBSET_LE] Theorem
β’ βs t. FINITE t β§ s β t β SUM_SET s β€ SUM_SET t
[SUM_SET_THM] Theorem
β’ SUM_SET β
= 0 β§
βx s. FINITE s β SUM_SET (x INSERT s) = x + SUM_SET (s DELETE x)
[SUM_SET_UNION] Theorem
β’ βs t.
FINITE s β§ FINITE t β
SUM_SET (s βͺ t) = SUM_SET s + SUM_SET t β SUM_SET (s β© t)
[SUM_SET_count] Theorem
β’ SUM_SET (count n) = n * (n β 1) DIV 2
[SUM_SET_count_2] Theorem
β’ βn. 2 * SUM_SET (count n) = n * (n β 1)
[SUM_UNIV] Theorem
β’ π(:Ξ± + Ξ²) = IMAGE INL π(:Ξ±) βͺ IMAGE INR π(:Ξ²)
[SURJECTIVE_IFF_INJECTIVE] Theorem
β’ βs f.
FINITE s β§ IMAGE f s β s β
((βy. y β s β βx. x β s β§ f x = y) β
βx y. x β s β§ y β s β§ f x = f y β x = y)
[SURJECTIVE_IFF_INJECTIVE_GEN] Theorem
β’ βs t f.
FINITE s β§ FINITE t β§ CARD s = CARD t β§ IMAGE f s β t β
((βy. y β t β βx. x β s β§ f x = y) β
βx y. x β s β§ y β s β§ f x = f y β x = y)
[SURJ_CARD] Theorem
β’ βs. FINITE s β βt. SURJ f s t β FINITE t β§ CARD t β€ CARD s
[SURJ_COMPOSE] Theorem
β’ βf g s t u. SURJ f s t β§ SURJ g t u β SURJ (g β f) s u
[SURJ_CONG] Theorem
β’ βf g s t. (βx. x β s β f x = g x) β (SURJ f s t β SURJ g s t)
[SURJ_ELEMENT] Theorem
β’ βf s t x. SURJ f s t β§ x β s β f x β t
[SURJ_EMPTY] Theorem
β’ βf. (βs. SURJ f β
s β s = β
) β§ βs. SURJ f s β
β s = β
[SURJ_ID] Theorem
β’ βs. SURJ (Ξ»x. x) s s
[SURJ_IMAGE] Theorem
β’ SURJ f s (IMAGE f s)
[SURJ_IMP_INJ] Theorem
β’ βs t. (βf. SURJ f s t) β βg. INJ g t s
[SURJ_INJ_INV] Theorem
β’ SURJ f s t β βg. INJ g t s β§ βy. y β t β f (g y) = y
[TC_PSUBSET] Theorem
β’ $PSUBSETβΊ = $PSUBSET
[TC_SUBSET_THM] Theorem
β’ $SUBSETβΊ = $SUBSET
[UNION_ASSOC] Theorem
β’ βs t u. s βͺ (t βͺ u) = s βͺ t βͺ u
[UNION_COMM] Theorem
β’ βs t. s βͺ t = t βͺ s
[UNION_DELETE] Theorem
β’ βA B x. A βͺ B DELETE x = A DELETE x βͺ (B DELETE x)
[UNION_DIFF] Theorem
β’ s β t β s βͺ (t DIFF s) = t β§ t DIFF s βͺ s = t
[UNION_DIFF_2] Theorem
β’ βs t. s βͺ (s DIFF t) = s
[UNION_DIFF_EQ] Theorem
β’ (βs t. s βͺ (t DIFF s) = s βͺ t) β§ βs t. t DIFF s βͺ s = t βͺ s
[UNION_EMPTY] Theorem
β’ (βs. β
βͺ s = s) β§ βs. s βͺ β
= s
[UNION_IDEMPOT] Theorem
β’ βs. s βͺ s = s
[UNION_OVER_INTER] Theorem
β’ βs t u. s β© (t βͺ u) = s β© t βͺ s β© u
[UNION_SUBSET] Theorem
β’ βs t u. s βͺ t β u β s β u β§ t β u
[UNION_UNIV] Theorem
β’ (βs. π(:Ξ±) βͺ s = π(:Ξ±)) β§ βs. s βͺ π(:Ξ±) = π(:Ξ±)
[UNION_applied] Theorem
β’ βs t x. (s βͺ t) x β x β s β¨ x β t
[UNIQUE_MEMBER_SING] Theorem
β’ βx s. x β s β§ (βy. y β s β x = y) β s = {x}
[UNIV_BOOL] Theorem
β’ π(:bool) = {T; F}
[UNIV_FUNSET_UNIV] Theorem
β’ FUNSET π(:Ξ±) π(:Ξ²) = π(:Ξ± -> Ξ²)
[UNIV_FUN_TO_BOOL] Theorem
β’ π(:Ξ± -> bool) = POW π(:Ξ±)
[UNIV_NOT_EMPTY] Theorem
β’ π(:Ξ±) β β
[UNIV_SUBSET] Theorem
β’ βs. π(:Ξ±) β s β s = π(:Ξ±)
[UNIV_applied] Theorem
β’ βx. π(:Ξ±) x
[X_LE_MAX_SET] Theorem
β’ βs. FINITE s β βx. x β s β x β€ MAX_SET s
[bigunion_countable] Theorem
β’ βs. countable s β§ (βx. x β s β countable x) β
countable (BIGUNION s)
[chooser_compute] Theorem
β’ (βs. chooser s 0 = CHOICE s) β§
(βs n.
chooser s <..num comp'n..> =
chooser (REST s) (<..num comp'n..> β 1)) β§
βs n.
chooser s <..num comp'n..> = chooser (REST s) <..num comp'n..>
[compl_insert] Theorem
β’ βs x. COMPL (x INSERT s) = COMPL s DELETE x
[count_EQN] Theorem
β’ βn. count n =
if n = 0 then β
else (let p = PRE n in p INSERT count p)
[count_add] Theorem
β’ βn m. count (n + m) = count n βͺ IMAGE ($+ n) (count m)
[count_add1] Theorem
β’ βn. count (n + 1) = n INSERT count n
[countable_EMPTY] Theorem
β’ countable β
[countable_INSERT] Theorem
β’ countable (x INSERT s) β countable s
[countable_Uprod] Theorem
β’ countable π(:Ξ± # Ξ²) β countable π(:Ξ±) β§ countable π(:Ξ²)
[countable_Usum] Theorem
β’ countable π(:Ξ± + Ξ²) β countable π(:Ξ±) β§ countable π(:Ξ²)
[countable_image_nats] Theorem
β’ countable (IMAGE f π(:num))
[countable_surj] Theorem
β’ βs. countable s β s = β
β¨ βf. SURJ f π(:num) s
[cross_countable] Theorem
β’ βs t. countable s β§ countable t β countable (s Γ t)
[cross_countable_IFF] Theorem
β’ countable (s Γ t) β s = β
β¨ t = β
β¨ countable s β§ countable t
[disjUNION_EQ_EMPTY] Theorem
β’ x β y = β
β x = β
β§ y = β
[disjUNION_UNIV] Theorem
β’ π(:Ξ± + Ξ²) = π(:Ξ±) β π(:Ξ²)
[disjointD] Theorem
β’ βA a b. disjoint A β a β A β b β A β a β b β DISJOINT a b
[disjointI] Theorem
β’ βA. (βa b. a β A β b β A β a β b β DISJOINT a b) β disjoint A
[disjoint_def] Theorem
β’ βA. disjoint A β βa b. a β A β§ b β A β§ a β b β DISJOINT a b
[disjoint_empty] Theorem
β’ disjoint β
[disjoint_image] Theorem
β’ βf. (βi j. i β j β DISJOINT (f i) (f j)) β disjoint (IMAGE f π(:Ξ±))
[disjoint_insert] Theorem
β’ βe c.
disjoint c β§ (βx. x β c β DISJOINT x e) β disjoint (e INSERT c)
[disjoint_insert_imp] Theorem
β’ βe c. disjoint (e INSERT c) β disjoint c
[disjoint_insert_notin] Theorem
β’ βe c. disjoint (e INSERT c) β§ e β c β βs. s β c β DISJOINT e s
[disjoint_restrict] Theorem
β’ βe c. disjoint c β disjoint (IMAGE ($INTER e) c)
[disjoint_same] Theorem
β’ βs t. s = t β disjoint {s; t}
[disjoint_sing] Theorem
β’ βa. disjoint {a}
[disjoint_two] Theorem
β’ βs t. s β t β§ DISJOINT s t β disjoint {s; t}
[disjoint_union] Theorem
β’ βA B.
disjoint A β§ disjoint B β§ BIGUNION A β© BIGUNION B = β
β
disjoint (A βͺ B)
[empty_partitions] Theorem
β’ βs. β
partitions s β s = β
[empty_refines] Theorem
β’ βv. β
refines v
[equiv_class_eq] Theorem
β’ βR s x y.
R equiv_on s β§ x β s β§ y β s β
(equiv_class R s x = equiv_class R s y β R x y)
[equiv_on_subset] Theorem
β’ βR s t. R equiv_on s β§ t β s β R equiv_on t
[equivalence_same_part] Theorem
β’ equivalence (Ξ»x y. part v x = part v y)
[finite_countable] Theorem
β’ βs. FINITE s β countable s
[image_countable] Theorem
β’ βf s. countable s β countable (IMAGE f s)
[in_max_set] Theorem
β’ βs. FINITE s β βx. x β s β x β€ MAX_SET s
[in_part] Theorem
β’ βw v x. v partitions w β§ x β w β x β part v x
[infinite_num_inj] Theorem
β’ βs. INFINITE s β βf. INJ f π(:num) s
[infinite_pow_uncountable] Theorem
β’ βs. INFINITE s β Β¬countable (POW s)
[infinite_rest] Theorem
β’ βs. INFINITE s β INFINITE (REST s)
[inj_countable] Theorem
β’ βf s t. countable t β§ INJ f s t β countable s
[inj_image_countable_IFF] Theorem
β’ INJ f s (IMAGE f s) β (countable (IMAGE f s) β countable s)
[inj_surj] Theorem
β’ βf s t. INJ f s t β s = β
β¨ βf'. SURJ f' t s
[inter_countable] Theorem
β’ βs t. countable s β¨ countable t β countable (s β© t)
[inv_image_equiv_on] Theorem
β’ βR Y f. R equiv_on Y β inv_image R f equiv_on {x | f x β Y}
[is_measure_maximal_INSERT] Theorem
β’ βx s m e y.
x β s β§ m e < m x β
(is_measure_maximal m (e INSERT s) y β is_measure_maximal m s y)
[is_measure_maximal_SING] Theorem
β’ is_measure_maximal m {x} y β y = x
[num_FINITE] Theorem
β’ βs. FINITE s β βa. βx. x β s β x β€ a
[num_FINITE_AVOID] Theorem
β’ βs. FINITE s β βa. a β s
[num_INFINITE] Theorem
β’ INFINITE π(:num)
[num_countable] Theorem
β’ countable π(:num)
[pair_to_num_formula] Theorem
β’ βx y. pair_to_num (x,y) = (x + y + 1) * (x + y) DIV 2 + y
[pair_to_num_inv] Theorem
β’ (βx. pair_to_num (num_to_pair x) = x) β§
βx y. num_to_pair (pair_to_num (x,y)) = (x,y)
[pair_to_num_inv'] Theorem
β’ (βx. pair_to_num (num_to_pair x) = x) β§
βx. num_to_pair (pair_to_num x) = x
[pairwise_EMPTY] Theorem
β’ βr. pairwise r β
[pairwise_SUBSET] Theorem
β’ βR s t. pairwise R t β§ s β t β pairwise R s
[pairwise_UNION] Theorem
β’ pairwise R (s1 βͺ s2) β
pairwise R s1 β§ pairwise R s2 β§
βx y. x β s1 β§ y β s2 β R x y β§ R y x
[part_SING] Theorem
β’ βx w. x β w β part {w} x = w
[part_in_partition] Theorem
β’ βw v x. v partitions w β§ x β w β part v x β v
[part_partition] Theorem
β’ βR w y.
y β w β§ R equiv_on w β
part (partition R w) y = {x | x β w β§ R x y}
[part_unique] Theorem
β’ βw v x s. v partitions w β§ x β w β§ x β s β§ s β v β s = part v x
[partition_CARD] Theorem
β’ βR s. R equiv_on s β§ FINITE s β CARD s = β CARD (partition R s)
[partition_SUBSET] Theorem
β’ βR s t. t β partition R s β t β s
[partition_elements_disjoint] Theorem
β’ R equiv_on s β
βt1 t2.
t1 β partition R s β§ t2 β partition R s β§ t1 β t2 β
DISJOINT t1 t2
[partition_elements_interrelate] Theorem
β’ R equiv_on s β βt. t β partition R s β βx y. x β t β§ y β t β R x y
[partition_rel_eq] Theorem
β’ βR1 R2 Y.
R1 equiv_on Y β§ R2 equiv_on Y β§ partition R1 Y = partition R2 Y β
βx y. x β Y β§ y β Y β (R1 x y β R2 x y)
[partitions_DISJOINT] Theorem
β’ βv w s1 s2.
v partitions w β§ s1 β v β§ s2 β v β§ s1 β s2 β DISJOINT s1 s2
[partitions_FINITE] Theorem
β’ βX Y. X partitions Y β§ FINITE Y β FINITE X β§ βs. s β X β FINITE s
[partitions_INSERT] Theorem
β’ βx w v.
x β w β
(v partitions x INSERT w β
βu s.
u partitions w β§ v = (x INSERT s) INSERT u DELETE s β§
(s β β
β s β u))
[partitions_PAIR_DISJOINT] Theorem
β’ βx y.
x partitions y β
β
β x β§ (βs t. s β x β§ t β x β§ s β t β DISJOINT s t) β§
BIGUNION x = y
[partitions_SING] Theorem
β’ βv x. SING x β (v partitions x β v = {{CHOICE x}})
[partitions_covers] Theorem
β’ βx y. x partitions y β BIGUNION x = y
[partitions_empty] Theorem
β’ βv. v partitions β
β v = β
[partitions_inj] Theorem
β’ βx w1 w2. x partitions w1 β§ x partitions w2 β w1 = w2
[partitions_thm] Theorem
β’ βX Y.
X partitions Y β
(βx. x β X β x β β
β§ x β Y) β§ βy. y β Y β β!x. x β X β§ y β x
[pow_no_surj] Theorem
β’ βs. Β¬βf. SURJ f s (POW s)
[prime_PROD_IMAGE] Theorem
β’ βf s.
FINITE s β
(prime (Ξ f s) β
βp. IMAGE f s β {1; p} β§ prime p β§ β!x. x β s β§ f x = p)
[refines_antisym] Theorem
β’ βw v1 v2.
v1 partitions w β§ v2 partitions w β§ v1 refines v2 β§ v2 refines v1 β
v1 = v2
[refines_grows_parts] Theorem
β’ βw v1 v2.
v1 partitions w β§ v2 partitions w β
(v1 refines v2 β
βx y.
x β w β§ y β w β§ part v1 x = part v1 y β part v2 x = part v2 y)
[refines_refl] Theorem
β’ βv. v refines v
[refines_transitive] Theorem
β’ βv1 v2 v3. v1 refines v2 β§ v2 refines v3 β v1 refines v3
[subset_countable] Theorem
β’ βs t. countable s β§ t β s β countable t
[transitive_PSUBSET] Theorem
β’ transitive $PSUBSET
[union_countable] Theorem
β’ βs t. countable s β§ countable t β countable (s βͺ t)
[union_countable_IFF] Theorem
β’ countable (s βͺ t) β countable s β§ countable t
*)
end
HOL 4, Trindemossen-2