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 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 count_def : thm
val countable_def : 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 partition_def : thm
val schroeder_close_def : thm
(* Theorems *)
val ABSORPTION : thm
val ABSORPTION_RWT : thm
val ABS_DIFF_SUM_IMAGE : thm
val BIGINTER_EMPTY : 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_EMPTY : thm
val BIGUNION_EQ_EMPTY : 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_DELETE : thm
val BIJ_EMPTY : thm
val BIJ_FINITE : thm
val BIJ_FINITE_SUBSET : thm
val BIJ_ID : thm
val BIJ_IFF_INV : thm
val BIJ_IMAGE : 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_LINV_BIJ : thm
val BIJ_LINV_INV : thm
val BIJ_NUM_COUNTABLE : thm
val BIJ_SYM : thm
val BIJ_SYM_IMP : thm
val BIJ_TRANS : thm
val BIJ_support : thm
val CARD_BIGUNION_SAME_SIZED_SETS : 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_IMAGE : thm
val CARD_INJ_IMAGE : thm
val CARD_INSERT : thm
val CARD_INTER_LESS_EQ : thm
val CARD_POW : 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_EQN : thm
val CARD_UNION_LE : thm
val CHOICE_INSERT_REST : 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_MONO : thm
val COUNT_NOT_EMPTY : thm
val COUNT_SUC : thm
val COUNT_ZERO : thm
val COUNT_applied : 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_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_SYM : 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 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_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_INDUCT : thm
val FINITE_INJ : thm
val FINITE_INSERT : thm
val FINITE_INTER : thm
val FINITE_ISO_NUM : thm
val FINITE_POW : thm
val FINITE_PREIMAGE : thm
val FINITE_PSUBSET_INFINITE : thm
val FINITE_PSUBSET_UNIV : thm
val FINITE_REST : thm
val FINITE_REST_EQ : 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 FORALL_IN_BIGUNION : thm
val FORALL_IN_IMAGE : thm
val FORALL_IN_INSERT : thm
val FORALL_IN_UNION : 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 IMAGE_11 : thm
val IMAGE_11_INFINITE : thm
val IMAGE_BIGUNION : thm
val IMAGE_COMPOSE : thm
val IMAGE_CONG : 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_I : thm
val IMAGE_ID : thm
val IMAGE_II : thm
val IMAGE_IMAGE : thm
val IMAGE_IN : thm
val IMAGE_INSERT : thm
val IMAGE_INTER : thm
val IMAGE_PREIMAGE : thm
val IMAGE_SING : thm
val IMAGE_SUBSET : thm
val IMAGE_SUBSET_gen : thm
val IMAGE_SURJ : thm
val IMAGE_UNION : thm
val IMAGE_applied : 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_DELETE : thm
val INJ_EMPTY : thm
val INJ_EXTEND : thm
val INJ_ID : thm
val INJ_IFF : thm
val INJ_IMAGE : thm
val INJ_IMAGE_BIJ : thm
val INJ_IMAGE_SUBSET : thm
val INJ_INL : thm
val INJ_INR : thm
val INJ_INSERT : thm
val INJ_LINV_OPT : thm
val INJ_LINV_OPT_IMAGE : thm
val INJ_SUBSET : 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_COMM : thm
val INTER_EMPTY : thm
val INTER_FINITE : thm
val INTER_IDEMPOT : thm
val INTER_OVER_UNION : 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 ITSET_EMPTY : thm
val ITSET_IND : thm
val ITSET_INSERT : thm
val ITSET_THM : thm
val ITSET_def : thm
val ITSET_ind : 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_REWRITES : thm
val MAX_SET_THM : thm
val MAX_SET_UNION : thm
val MEMBER_NOT_EMPTY : thm
val MIN_SET_ELIM : thm
val MIN_SET_LEM : thm
val MIN_SET_LEQ_MAX_SET : 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_SET_WOP : 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 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 PROD_IMAGE_THM : thm
val PROD_SET_EMPTY : thm
val PROD_SET_IMAGE_REDUCTION : 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 REL_RESTRICT_EMPTY : thm
val REL_RESTRICT_SUBSET : thm
val REST_PSUBSET : thm
val REST_SING : thm
val REST_SUBSET : thm
val REST_applied : thm
val RINV_DEF : 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 SING : thm
val SING_DELETE : 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_UNION : thm
val SING_applied : thm
val SPECIFICATION : thm
val SUBSET_ADD : thm
val SUBSET_ANTISYM : thm
val SUBSET_BIGINTER : thm
val SUBSET_BIGUNION_I : 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_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_SUBSET_EQ : 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 SUM_IMAGE_CONG : thm
val SUM_IMAGE_DELETE : thm
val SUM_IMAGE_INJ_o : thm
val SUM_IMAGE_IN_LE : thm
val SUM_IMAGE_MONO_LESS : thm
val SUM_IMAGE_MONO_LESS_EQ : 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_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_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 SURJ_CARD : thm
val SURJ_COMPOSE : thm
val SURJ_EMPTY : thm
val SURJ_ID : thm
val SURJ_IMAGE : thm
val SURJ_IMP_INJ : thm
val SURJ_INJ_INV : thm
val UNION_ASSOC : thm
val UNION_COMM : thm
val UNION_DELETE : thm
val UNION_DIFF : thm
val UNION_DIFF_2 : 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 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 finite_countable : thm
val image_countable : thm
val in_max_set : 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 is_measure_maximal_INSERT : thm
val is_measure_maximal_SING : thm
val num_countable : thm
val pair_to_num_formula : thm
val pair_to_num_inv : thm
val pairwise_SUBSET : thm
val pairwise_UNION : thm
val partition_CARD : thm
val partition_SUBSET : thm
val partition_elements_disjoint : thm
val partition_elements_interrelate : thm
val pow_no_surj : thm
val subset_countable : thm
val union_countable : thm
val union_countable_IFF : thm
val pred_set_grammars : type_grammar.grammar * term_grammar.grammar
val SET_SPEC_ss : simpLib.ssfrag
(*
[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
[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
[count_def] Definition
⊢ ∀n. count n = {m | m < n}
[countable_def] Definition
⊢ ∀s. countable s ⇔ ∃f. INJ f s 𝕌(:num)
[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
[partition_def] Definition
⊢ ∀R s. partition R s = {t | ∃x. x ∈ s ∧ t = {y | y ∈ s ∧ R x y}}
[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_EMPTY] Theorem
⊢ BIGINTER ∅ = 𝕌(:α)
[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) ∧ s ≠ ∅ ⇒ 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_EMPTY] Theorem
⊢ BIGUNION ∅ = ∅
[BIGUNION_EQ_EMPTY] Theorem
⊢ ∀P.
(BIGUNION P = ∅ ⇔ P = ∅ ∨ P = {∅}) ∧
(∅ = BIGUNION P ⇔ P = ∅ ∨ P = {∅})
[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_DELETE] Theorem
⊢ ∀s t f. BIJ f s t ⇒ ∀e. e ∈ s ⇒ BIJ f (s DELETE e) (t DELETE f e)
[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_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_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_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_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_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_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_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
⊢ ∀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_IMAGE] Theorem
⊢ ∀s. FINITE s ⇒ CARD (IMAGE f 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_POW] Theorem
⊢ ∀s. FINITE s ⇒ CARD (POW s) = 2 ** CARD s
[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_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
[CHOICE_INSERT_REST] Theorem
⊢ ∀s. s ≠ ∅ ⇒ CHOICE s INSERT REST s = 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_MONO] Theorem
⊢ ∀m n. m ≤ n ⇒ count m ⊆ count n
[COUNT_NOT_EMPTY] Theorem
⊢ ∀n. 0 < n ⇔ count n ≠ ∅
[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_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_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_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_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
[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_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_INDUCT] Theorem
⊢ ∀P.
P ∅ ∧ (∀s. FINITE s ∧ P s ⇒ ∀e. e ∉ s ⇒ P (e 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_POW] Theorem
⊢ ∀s. FINITE s ⇒ FINITE (POW s)
[FINITE_PREIMAGE] Theorem
⊢ (∀x y. f x = f y ⇔ x = y) ∧ FINITE s ⇒ FINITE (PREIMAGE f s)
[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_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
⊢ ∀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
[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
[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} = 𝕌(:α)
[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_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_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_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_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_SING] Theorem
⊢ ∀f x. IMAGE f {x} = {f x}
[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
[INFINITE_DIFF_FINITE] Theorem
⊢ ∀s t. INFINITE s ∧ FINITE t ⇒ 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_DELETE] Theorem
⊢ ∀f s t. INJ f s t ⇒ ∀e. e ∈ s ⇒ INJ f (s DELETE e) (t DELETE f e)
[INJ_EMPTY] Theorem
⊢ ∀f. (∀s. INJ f ∅ s) ∧ ∀s. INJ f s ∅ ⇔ s = ∅
[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_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_SUBSET] Theorem
⊢ ∀f s t. INJ f s t ⇒ IMAGE f s ⊆ t
[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_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
[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_COMM] Theorem
⊢ ∀s t. s ∩ t = t ∩ s
[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_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 ∈ 𝕌(:α)
[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_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
[ITSET_ind] Theorem
⊢ ∀P.
(∀s b. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s) (f (CHOICE s) b)) ⇒ P s b) ⇒
∀v v1. P v v1
[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_REWRITES] Theorem
⊢ MAX_SET ∅ = 0 ∧ MAX_SET {e} = e
[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_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_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_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_SET_WOP] Theorem
⊢ ∀s. (∃n. n ∈ s) ⇔ ∃n. n ∈ s ∧ ∀m. m ∈ s ⇒ n ≤ m
[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
[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_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
[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_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
[REL_RESTRICT_EMPTY] Theorem
⊢ REL_RESTRICT R ∅ = ∅ᵣ
[REL_RESTRICT_SUBSET] Theorem
⊢ s1 ⊆ s2 ⇒ REL_RESTRICT R s1 ⊆ᵣ REL_RESTRICT R s2
[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
[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
⊢ ∀s1 s2. s1 = s2 ⇔ s1 ⊆ s2 ∧ s2 ⊆ s1
[SET_MINIMUM] Theorem
⊢ ∀s M. (∃x. x ∈ s) ⇔ ∃x. x ∈ s ∧ ∀y. y ∈ s ⇒ M x ≤ M y
[SING] Theorem
⊢ ∀x. SING {x}
[SING_DELETE] Theorem
⊢ ∀x. {x} DELETE x = ∅
[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_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
[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_BIGINTER] Theorem
⊢ ∀X P. X ⊆ BIGINTER P ⇔ ∀Y. Y ∈ P ⇒ X ⊆ Y
[SUBSET_BIGUNION_I] Theorem
⊢ ∀x P. x ∈ P ⇒ x ⊆ BIGUNION P
[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_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 n. 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_SUBSET_EQ] Theorem
⊢ ∀s t. s ⊆ t ∧ t ⊆ s ⇔ s = t
[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
[SUM_IMAGE_CONG] Theorem
⊢ s1 = s2 ∧ (∀x. x ∈ s2 ⇒ f1 x = f2 x) ⇒ ∑ f1 s1 = ∑ f2 s2
[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_INJ_o] Theorem
⊢ ∀s.
FINITE s ⇒
∀g. INJ g s 𝕌(:α) ⇒ ∀f. ∑ f (IMAGE g s) = ∑ (f ∘ g) 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_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_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_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 𝕌(:β)
[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_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
[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_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
[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 (NUMERAL (BIT1 n)) =
chooser (REST s) (NUMERAL (BIT1 n) − 1)) ∧
∀s n.
chooser s (NUMERAL (BIT2 n)) =
chooser (REST s) (NUMERAL (BIT1 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
[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
[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)
[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_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)
[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
[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
[pow_no_surj] Theorem
⊢ ∀s. ¬∃f. SURJ f s (POW s)
[subset_countable] Theorem
⊢ ∀s t. countable s ∧ t ⊆ s ⇒ countable t
[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, Kananaskis-13