IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Nuprl Section: DiscreteMath - Discrete Math Lessons

 Introduction Introductory Remarks def is_one_one_corr_rel One-one correlation as a relation 1-1-Corr x:A,y:B. R(x;y) == (x:A. !y:B. R(x;y)) & (y:B. !x:A. R(x;y)) def is_list_mem (a is a member of list xs) a  xs == Case of xs; nil  False ; x.ys  a = x  A  (a  ys)  (recursive) THM ndiff_vs_diff a,b:. ab  (b -- a) = b-a THM eq_int_is_eq_nsub IsEqFun(b;i,j. i=j) THM decidable__nat_equal i,j:. Dec(i = j) THM exteq_singleton_vs_intseg a,a':. a'-a = 1  ({a..a'} =ext {a:}) THM exteq_prod_family_singleton_vs_intseg a,a':. a'-a = 1  (B:({a..a'}Type{i}). (i:{a..a'}B(i)) =ext ({a:}B(a))) THM exteq_sum_family_singleton_vs_intseg a,a':. a'-a = 1  (B:({a..a'}Type{i}). (i:{a..a'}B(i)) =ext ({a:}B(a))) def injection_type (the injections from A into B) A inj B == {f:(AB)| Inj(A; B; f) } def bijection_type (the bijections from A onto B) A bij B == {f:(AB)| Bij(A; B; f) } THM injtype_vs_inj ((A inj B))  (f:(AB). Inj(A; B; f)) THM injection_type_fun f:(A inj B). f  AB THM injection_type_injection f:(A inj B). Inj(A; B; f) THM inj_point_deletion f:(A inj B), a:A. f  {x:A| x = a }{y:B| y = f(a) } THM inj_point_deletion_inj f:(A inj B), a:A. f  {x:A| x = a } inj {y:B| y = f(a) } THM inj_from_empty_unique (A)  (!(A inj B)) THM bijtype_sub_injtype (A bij B)  (A inj B) THM bijection_type_inc_inj (A bij B)  (A inj B) THM nsub_inj_lop_typing a:, b:, f:(a inj b). f  (a-1) inj {x:b| x = f(a-1) } THM nsub_inj_fill_typing a:, b:, j:b, f:((a-1) inj {x:b| x = j }). (i.if i=a-1 j else f(i) fi)  a inj b def surjection_type (the surjections from A onto B) A onto B == {f:(AB)| Surj(A; B; f) } THM bijtype_sub_surjtype (A bij B)  (A onto B) THM bijection_type_inc_surj (A bij B)  (A onto B) THM bijtype_exteq_inj_isect_surjtype (A bij B) =ext ((A inj B)(A onto B)) COM unicomp_assoc h o g o f = h o g o f ... COM inverse_function_intro Explain inverse functions and Def  InvFuns(A; B; f; g) == g o f = Id & f o g = Id COM one_one_corr_intro One-to-One Correspondence ... COM one_one_corr_via_inverse One-to-One Correspondence via Inverse Functions ... COM one_one_corr_intro_aux1 Comparison of definitional resources used. ... COM one_one_corr_intro3 One-to-One Correspondence: equivalence of two characterizations. ... COM count_demo Counting is finding a function of a certain kind. ... def list_to_function A function mapping positions in a list to entries seq:l(i) == l[i] COM note_on_generalization_for_induction Not done yet. def replace_fn_values (Replace values x s.t. P(x) by y in f)(i) == if P(f(i)) y else f(i) fi def delete_fenum_value Special purpose operation for shrinking the domain and range of an injection simultaneously. See REMARK. Replace value k by f(m) in f == Replace values x s.t. x=k by f(m) in f COM delete_fenum_value_example let xs = [1; 3; 0; 7; 2; 4; 6; 5] in  let v = 4 in (Replace value v by seq:xs(||xs||-1) in seq:xs){(||xs||-1)} * [1; 3; 0; 7; 2; 5; 6] THM delete_fenum_value_comp1_gen Inj({u:| P(u) }; {u:| Q(u) }; f) (m:{u:| P(u) }, k:{v:| Q(v) }, i:{u:| P(u) & u = m }. (f(i) = k  (Replace value k by f(m) in f)(i) = f(m)  {v:| Q(v) & v = k }) THM delete_fenum_value_comp2_gen Inj({u:| P(u) }; {u:| Q(u) }; f) (m:{u:| P(u) }, k:{v:| Q(v) }, i:{u:| P(u) & u = m }. (f(i) = k  (Replace value k by f(m) in f)(i) = f(i)  {v:| Q(v) & v = k }) THM delete_fenum_value_is_inj_genW Inj({u:| P(u) }; {v:| Q(v) }; f) (m:{u:| P(u) }, k:{v:| Q(v) }. ((Replace value k by f(m) in f)  {u:| P(u) & u = m }{v:| Q(v) & v = k } (& Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k }; (& Inj(Replace value k by f(m) in f)) THM delete_fenum_value_is_inj_gen Inj({u:| P(u) }; {v:| Q(v) }; f) (m:{u:| P(u) }, k:{v:| Q(v) }. (Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k }; (Inj(Replace value k by f(m) in f)) THM delete_fenum_value_is_fenum_gen Bij({u:| P(u) }; {v:| Q(v) }; f) (m:{u:| P(u) }, k:{v:| Q(v) }. (Bij({u:| P(u) & u = m }; {v:| Q(v) & v = k }; (Bij(Replace value k by f(m) in f)) THM delete_fenum_value_comp1 Inj((m+1); (k+1); f) (i:m. f(i) = k  (Replace value k by f(m) in f)(i) = f(m) k) THM delete_fenum_value_comp2 Inj((m+1); (k+1); f) (i:m. f(i) = k  (Replace value k by f(m) in f)(i) = f(i) k) THM delete_fenum_value_is_inj Inj((m+1); (k+1); f)  Inj(m; k; Replace value k by f(m) in f) THM delete_fenum_value_is_fenum Bij((m+1); (k+1); f)  Bij(m; k; Replace value k by f(m) in f) THM finite_inj_counter_example (Proof Gloss) Lemma for the pigeon-hole principle. A finite non-injection into integers maps some two distinct arguments to the same value. m:, f:(m). Inj(m; ; f)  (x:m, y:x. f(x) = f(y)) THM inj_imp_le (Proof Gloss) The range of a finite injection is as big as its domain. (f:(mk). Inj(m; k; f))  mk THM inj_typing_imp_le The range of a finite injection is as big as its domain. ((m inj k))  mk THM inj_imp_le2 The range of a finite injection is as big as its domain. m,k:, f:(mk). Inj(m; k; f)  mk THM pigeon_hole (Proof Gloss) The pigeon-hole principle A mapping from one finite collection into a smaller collection assigns a single output to two inputs. m,k:, f:(mk). k; b. <1,b>) def sigma_to_union sigma_to_union(e) == e/i,u. if i=0 inl(u) else inr(u) fi def inv_pair (the inverse function pairs between A and B) AB == {fg:((AB)(BA))| fg/f,g. InvFuns(A;B;f;g) } THM inv_pair_iff_ooc ((AB))  (A ~ B) def fin_enum (the finite enumerations of A) fin_enum(A) == k:kA THM factorial_via_intseg_zero 0! THM factorial_via_intseg_step k,n:. k = n+1  k! = kn! THM factorial_via_intseg_step_rw k:. k! = k(k-1)! def unboundedly_infinite (one can find any number of members of A) Unbounded(A) == k:. (k inj A) def productively_infinite (there is an infinite (omega) sequence of distinct members of A) Infinite(A) == ( inj A) THM unboundedly_imp_productively_infinite Infinite(A)  Unbounded(A) def Dedekind_infinite Dedekind's formulation of infinite class (A can be mapped 1-1 into a proper subpart of itself) Dedekind-Infinite(A) == a:A, f:(AA). Inj(A; A; f) & (x:A. f(x) = a) THM ndiff_bound b,a:. b(b -- a)+a THM eq_mem_is_ax a,a':A, x:(a = a'). x = * THM comp_preserves_inj Composing injections gives an injection. Inj(A; B; g)  Inj(B; C; f)  Inj(A; C; f o g) THM comp_preserves_surj Composing surjections gives a surjection. Surj(A; B; g)  Surj(B; C; f)  Surj(A; C; f o g) THM surjection_type_surjection f:(A onto B), a:. a onto A  (B Discrete)  Surj(A; B; f) THM surjection_type_nsub_surjection f:(a onto b). Surj(a; b; f) THM inv_pair_functionality_wrt_one_one_corr (A ~ A')  (B ~ B')  ((AB) ~ (A'B')) THM one_one_corr_fams_trans One-to-one correspondence between indexed families of classes is transitive. A:Type, A',A'':Type, B:(AType), B':(A'Type), B'':(A''Type). (x:A. B(x)) ~ (x':A'. B'(x')) (x':A'. B'(x')) ~ (x'':A''. B''(x''))  (x:A. B(x)) ~ (x'':A''. B''(x'')) THM comp_preserves_bij Composing bijections gives a bijection. Bij(A; B; g)  Bij(B; C; f)  Bij(A; C; f o g) THM one_one_corr_rel_vs_invfuns Equivalence of one-one correspondence and existence of inverses R:(ABProp).  (1-1-Corr x:A,y:B. R(x;y)) (f:(AB), g:(BA). (InvFuns(A;B;f;g) & (x:A, y:B. R(x;y)  y = f(x) & x = g(y))) THM card_split_prod_intseg_family_decbl (x:A. Dec(P(x)))  ((x:AB(x)) ~ ((x:A st P(x)B(x))(x:A st P(x)B(x)))) THM finite_choice Principle of finite choice. The function can be constructed explicitly without appeal to the Axiom of Choice. k:, Q:(kAProp). (x:k. y:A. Q(x;y))  (f:(kA). x:k. Q(x;f(x))) THM dep_finite_choice Principle of dependent finite choice. The function can be constructed explicitly without appeal to the Dependent Axiom of Choice. k:, B:(kType), Q:(x:kB(x)Prop). (x:k. y:B(x). Q(x;y))  (f:(x:kB(x)). x:k. Q(x;f(x))) THM inv_funs_2_sym Being mutual inverses is symmetric. InvFuns(A;B;f;g)  InvFuns(B;A;g;f) THM invfuns_are_surj Mutually inverse functions are surjections. InvFuns(A;B;f;g)  Surj(A; B; f) & Surj(B; A; g) THM surjection_type_functionality_wrt_ooc (A ~ A')  (B ~ B')  ((A onto B) ~ (A' onto B')) THM one_one_corr_fams_sym B:(AType), B':(A'Type). (x:A. B(x)) ~ (x':A'. B'(x'))  (x':A'. B'(x')) ~ (x:A. B(x)) THM fun_with_inv2_is_inj_rev InvFuns(A;B;f;g)  Inj(B; A; g) THM ooc_preserves_dededkind_inf (A ~ B)  Dedekind-Infinite(A)  Dedekind-Infinite(B) THM invfuns_are_inj Mutually inverse functions are injections. InvFuns(A;B;f;g)  Inj(A; B; f) & Inj(B; A; g) THM injection_type_functionality_wrt_ooc (A ~ A')  (B ~ B')  ((A inj B) ~ (A' inj B')) THM fun_with_inv2_is_surj_rev InvFuns(A;B;f;g)  Surj(B; A; g) THM one_one_corr_is_equiv_rel EquivRel X,Y:Type. X ~ Y THM iff_weakening_wrt_one_one_corr_2 (A ~ B)  (A  B) THM inhabited_functionality_wrt_one_one_corr (A ~ B)  ((A)  (B)) THM one_one_corr_2_functionality_wrt_one_one_corr (A ~ A')  (B ~ B')  ((A ~ B)  (A' ~ B')) THM one_one_corr_2_reflex A ~ A THM one_one_corr_2_inversion (A ~ B)  (B ~ A) THM one_one_corr_2_transitivity (A ~ B)  (B ~ C)  (A ~ C) COM one_one_corr_via_bijection One-to-One Correspondence via Bijection ... COM one_one_corr_and_bij_thm One-to-One Correspondence: equivalence of two characterizations. ... THM inv_funs_2_unique A function has at most one inverse. InvFuns(A;B;f;g)  InvFuns(A;B;f;h)  g = h THM left_inv_of_surj_is_right_inv A function that cancels a surjection is also cancelled by it. g:(BA). Surj(A; B; f)  (x:A. g(f(x)) = x)  (y:B. f(g(y)) = y) THM parallel_conjunct_imp (A  C)  (B  D)  A & B  C & D THM fun_with_inv2_is_bij (Proof Gloss) InvFuns(A;B;f;g)  Bij(A; B; f) THM fun_with_inv2_is_bij_rev InvFuns(A;B;f;g)  Bij(B; A; g) THM comp_id_r_version2 f:(AB). f o Id = f  AB THM comp_id_l_version2 f:(AB). Id o f = f  AB THM comp_assoc_version2 f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f  AD THM eta_conv_version2 f:(AB). (x.f(x)) = f THM fun_with_inv_is_bij_version2 f:(AB), g:(BA). InvFuns(A;B;f;g)  Bij(A; B; f) THM bij_imp_exists_inv_version2 Bijections have inverses. f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A;B;f;g)) THM bij_iff_1_1_corr_version2 (f:(AB). Bij(A; B; f))  (A ~ B) THM int_ooc_nat There are as many non-negative integers as integers.  ~ THM unb_inf_not_fin Unbounded(A)  Finite(A) THM infinite_imp_nonfinite Infinite(A)  Finite(A) THM ooc_preserves_unb_inf (A ~ B)  Unbounded(A)  Unbounded(B) THM ooc_preserves_infiniteness (A ~ B)  Infinite(A)  Infinite(B) THM bij_iff_1_1_corr_version2a (f:(AB). Bij(A; B; f))  (B ~ A) THM negnegelim_imp_notfin_imp_unb_inf (P:Prop. P  P)  (A:Type. Finite(A)  Unbounded(A)) THM nsub_not_infinite k:. Infinite(k) THM absurd_nonfin_imp_unb_inf (A:Type. Finite(A)  Unbounded(A))  (D:Type. (D)  (D)) THM nonfin_eqv_unb_inf_iff_negnegelim (A:Type. Finite(A)  Unbounded(A))  (P:Prop. P  P) THM absurd_nonfinite_imp_infinite (A:Type. Finite(A)  Infinite(A))  (D:Type. (D)  (D)) THM not_nat_occ_natfuns The infinite sequences of numbers cannot be paired one-to-one with the numbers themselves. (Cantor) (() ~ ) THM counting_is_unique (Proof Gloss) Any way of counting a finite class produces the same number. (A ~ m)  (A ~ k)  m = k THM fin_card_vs_nat_eq a,b:. (a ~ b)  a = b THM nat_not_finite Finite() THM partition_type P:(ABProp). (x:A. !y:B. P(x;y))  (A ~ (y:B{x:A| P(x;y) })) THM bij_imp_exists_inv2 Bijections have inverses. f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A;B;f;g)) THM bij_iff_is_1_1_corr Bijections and one-one correspondence functions are the same. Bij(A; B; f)  f is 1-1 corr THM one_one_corr_fams_if_one_one_corr_B (x:A. B(x) ~ B'(x))  (x:A. B(x)) ~ (x:A. B'(x)) THM one_one_corr_fams_if_bij_A g:(A'A). Bij(A'; A; g)  (x:A. B(x)) ~ (x':A'. B(g(x'))) THM one_one_corr_fams_indep_if_one_one_corr (A ~ A')  (B ~ B')  (:A. B) ~ (:A'. B') THM union_functionality_wrt_one_one_corr (A ~ A')  (B ~ B')  ((A+B) ~ (A'+B')) def seq_nil Nil(i) == i def seq_cons [x/ xs](i) == if i=0 x else xs(i-1) fi THM card_product_swap (AB) ~ (BA) THM card_settype Bij(A; A'; f)  (x:A. B(x)  B'(f(x)))  ({x:A| B(x) } ~ {x:A'| B'(x) }) THM card_settype_sq Bij(A; A'; f)  (x:A. B(x)  B'(f(x)))  ({x:A| B(x) } ~ {x:A'| B'(x) }) THM set_functionality_wrt_one_one_corr_n_pred2 (x:A. B(x)  B'(x))  ({x:A| B(x) } ~ {x:A| B'(x) }) THM set_functionality_wrt_one_one_corr_n_pred (x:A. B(x)  B'(x))  ({x:A| B(x) } ~ {x:A| B'(x) }) THM card_sigma (x:A. B(x)) ~ (x:A'. B'(x))  ((x:AB(x)) ~ (x:A'B'(x))) THM product_functionality_wrt_one_one_corr_B B,B':(AType). (x:A. B(x) ~ B'(x))  ((x:AB(x)) ~ (x:AB'(x))) THM card_quotient (q:A/E{x:A| q = x  A/E }) ~ A THM product_functionality_wrt_one_one_corr (A ~ A')  (B ~ B')  ((AB) ~ (A'B')) THM card_split_prod_intseg_family a,b:, c:{a...b}, B:({a..b}Type). (i:{a..b}B(i)) ~ ((i:{a..c}B(i))(i:{c..b}B(i))) THM union_sigma_inverses InvFuns(A+B;i:2if i=0 A else B fi;union_to_sigma;sigma_to_union) THM card_union_swap (A+B) ~ (B+A) THM card_union_vs_sigma (A+B) ~ (i:2if i=0 A else B fi) THM card_split_decbl (x:A. Dec(P(x)))  (A ~ ({x:A| P(x) }+{x:A| P(x) })) THM card_sigma_st_dom B:(AType), P:(AProp). (i:{i:A| P(i) }B(i)) ~ {v:(i:AB(i))| P(v/x,y. x) } THM card_split_sigma_dom_decbl B:(AType), P:(AProp). (i:A. Dec(P(i))) ((i:AB(i)) ~ ((i:{i:A| P(i) }B(i))+(i:{i:A| P(i) }B(i)))) THM card_nsub0_union (0+A) ~ A THM card_nsub0_union_2 (A+0) ~ A THM card_split_decbl_squash (x:A. Dec(P(x)))  (A ~ ({x:A| P(x) }+{x:A| P(x) })) THM card_split_sum_intseg_family a,b:, c:{a...b}, B:({a..b}Type). (i:{a..b}B(i)) ~ ((i:{a..c}B(i))+(i:{c..b}B(i))) THM card_split_end_sum_intseg_family a,b:, B:({a..b}Type). a)) THM card_sigma_distr (xy:(x:AB(x))C(xy)) ~ (x:Ay:B(x)C()) THM intseg_void a,b:. ba  (Void ~ {a..b}) THM nsub_void Void ~ 0 THM intseg_shift a,b,a',b':. b-a = b'-a'  ({a..b} ~ {a'..b'}) THM intseg_shift_by a:, b,c:. {a..b} ~ {(a+c)..(b+c)} THM nsub_unit Unit ~ 1 THM nsub_bool ~ 2 THM nsub_intseg c,a:, b:. c = b-a  ({a..b} ~ c) THM nsub_intseg_rw a,b:. {a..b} ~ (b-a) THM intiseg_intseg a,b',b:. b = b'+1  ({a...b'} ~ {a..b}) THM intiseg_intseg_plus a:, b:. {a...b} ~ {a..(b+1)} THM nsub_intiseg_rw a,b:. {a...b} ~ (1+b-a) THM intseg_split a,b:, c:{a...b}. ({a..c}+{c..b}) ~ {a..b} THM nsub_add c,a,b:. a+b = c    ((a+b) ~ c) THM nsub_mul a,b,c:. ab = c  ((ab) ~ c) THM nsub_mul_rw a,b:. (ab) ~ (ab) THM mul_assoc_from_cross_assoc a,b,c:. a(bc) = (ab)c THM finite_indep_sum_card a,b:. (A ~ a)  (B ~ b)  ((AB) ~ (ab)) THM nsub_inj_factorial2 Relevant to permutation counting problems since these injections are the finite permutations. (b inj b) ~ (b!) THM nsub_inj_factorial_tail Relevant to so-called permutation counting problems since these injections are the ways to order a distinct values chosen from a total of b values. (a inj b) ~ (b!a) THM nsub_inj_factorial A more direct proof of this fact is in nsub inj factorial2. (k inj k) ~ (k!) THM card_pi_vs_nsub_pi The size of the general product space (whose members are functions) of a finite family of finite classes is the integer product of those classes' sizes. a:, b:(a). (i:ab(i)) ~ ( i:a. b(i)) THM card_fun_vs_nsub_exp Corollary to card pi vs nsub pi a,b:. (ab) ~ (ba) THM exp_exp_reduce1 a,b,c:. c(ab) = (cb)a THM exp_exp_reduce2 a,b,c:. c(ab) = (ca)b THM card_curry_simple2 (ABC) ~ (BAC) THM nsub_add_rw The size of the disjoint union of two finite classes is the sum of those classes' sizes. a,b:. (a+b) ~ (a+b) THM card_sigma_vs_nsub_sigma The size of a general sum (whose members are pairs) of a finite family of finite classes is the integer sum of those classes' sizes. a:, b:(a). (i:ab(i)) ~ ( i:a. b(i)) THM inv_pair_inv (AB) ~ (A ~ B) THM inv_pair_inv2 ((AB)) ~ (A ~ B) def next_nat_pair How to step from pair to pair exhaustively next_nat_pair(xy) == xy/x,y. if y=0 <0,x+1> else  fi THM next_nat_pair_not_zeroes The zero-zero pair does not succeed any other. xy:(). <0,0> = next_nat_pair(xy) THM next_nat_pair_inj Inj(; ; next_nat_pair) def prev_nat_pair Reverses next nat pair prev_nat_pair(xy) == xy/x,y. if x=0  else  fi THM next_nat_pair_vs_prev_nat_pair InvFuns(;{xy:()| xy = <0,0>   };next_nat_pair;prev_nat_pair) def nat_to_nat_pair (i steps of next_nat_pair from <0,0>) nat_to_nat_pair(i) == next_nat_pair{i}(<0,0>) THM nat_to_nat_pair_inj Inj(; ; nat_to_nat_pair) THM nat_to_nat_pair_surj Surj(; ; nat_to_nat_pair) THM nat_to_nat_pair_bij Bij(; ; nat_to_nat_pair) THM card_nat_vs_nat_nat The ordered pairs of natural numbers can be placed in one-to-one correspondence with the natural numbers. (Cantor) () ~ THM card_nat_vs_nat_tuple The k-tuples of natural numbers can be placed in one-to-one correspondence with the natural numbers theselves. k:. (k) ~ THM card_nat_vs_nat_tuples The finite nonempty sequences of natural numbers can be placed in one-one correspondence with the natural numbers themselves. (k:k) ~ THM card_nat_vs_nat_tuples_all The finite sequences of natural numbers can be placed in one-one correspondence with the natural numbers themselves. (k:k) ~ THM compose_iter_zero f:(AA), x:A. f{0}(x) = x THM compose_iter_zero_id f:(AA). f{0} = Id THM compose_iter_once f:(AA). f{1} = f THM compose_iter_pos f:(AA), i:, x:A. f{i}(x) = f(f{i-1}(x)) THM compose_iter_point_id f:(AA), u:A. f(u) = u  (i:. f{i}(u) = u) THM compose_iter_pos_comp f:(AA), i:. f{i} = f o f{i-1} THM compose_iter_id i:. Id{i} = Id  AA THM compose_iter_sum x:A, f:(AA), i,j,k:. k = i+j  f{i}(f{j}(x)) = f{k}(x) THM compose_iter_sum_comp f:(AA), i,j,k:. k = i+j  f{i} o f{j} = f{k} THM compose_iter_sum_rw x:A, f:(AA), k:, i:{0...k}. f{k}(x) = f{i}(f{k-i}(x)) THM compose_iter_sum_comp_rw f:(AA), k:, i:{0...k}. f{k} = f{i} o f{k-i} THM compose_iter_prod x:A, f:(AA), i,j,k:. k = ij  f{i}{j}(x) = f{k}(x)  A THM compose_iter_prod2 x:A, f:(AA), i,j:. f{i}{j}(x) = f{ij}(x) THM compose_iter_pos2 f:(AA), i:, x:A. f{i}(x) = f{i-1}(f(x)) THM compose_iter_pos_comp2 f:(AA), i:. f{i} = f{i-1} o f THM compose_iter_injection Iteration of an injection is an injection. Inj(A; A; f)  (i:. Inj(A; A; f{i})) THM compose_iter_inj_cycles A finite permutation always cycles back on each argument. k:, f:(k inj k), u:k. i:. f{i}(u) = u THM iter_perm_cycles_uniform Some positive iteration of any finite permutation is the identity function. k:, f:(k inj k). i:. u:k. f{i}(u) = u THM iter_perm_cycles_uniform2 Corollary of iter perm cycles uniform. Some positive iteration of any finite permutation is the identity function. k:, f:(k inj k). i:. f{i} = Id  kk THM compose_iter_injection2 f:(A inj A), i:. f{i}  A inj A THM compose_iter_surjection Iteration of a surjection is a surjection. Surj(A; A; f)  (i:. Surj(A; A; f{i})) THM compose_iter_bijection Iteration of a bijection is a bijection. Bij(A; A; f)  (i:. Bij(A; A; f{i})) THM compose_iter_inverses InvFuns(A;A;f;g)  (i:. InvFuns(A;A;f{i};g{i})) THM dedekind_inf_imp_inf Dedekind-Infinite(A)  Infinite(A) THM dededing_imp_unb_inf Dedekind-Infinite(A)  Unbounded(A) THM dedekind_imp_nonfin Dedekind-Infinite(A)  Finite(A) THM nsub_surj_imp_a_rev_inj_gen e:(BB).  IsEqFun(B;e)  (a:, f:(a onto B). (y.least x:. (f(x)) e y)  B inj a) THM nsub_surj_imp_a_rev_inj f:(a onto b). (y.least x:. f(x)=y)  b inj a THM nsub_bij_least_preimage_inverse f:(a bij a). InvFuns(a;a;f;y.least x:. f(x)=y) THM nsub_surj_imp_a_rev_inj2 ((a onto b))  ((b inj a)) THM surj_typing_imp_le ((a onto b))  ba THM nsub_inj_exteq_nsub_surj (k inj k) =ext (k onto k) THM nsub_surj_exteq_nsub_bij (k onto k) =ext (k bij k) THM nsub_surj_ooc_nsub_bij (k onto k) ~ (k bij k) THM nsub_inj_exteq_nsub_bij (k inj k) =ext (k bij k) THM nsub_inj_ooc_nsub_bij (k inj k) ~ (k bij k) THM nsub_inj_ooc_nsub_surj (k inj k) ~ (k onto k) THM nsub_bij_ooc_invpair (a bij a) ~ (aa) def msize The size of a finite multiset. Msize(f) ==  i:k. f(i) def sized_mset (multisets of size k) a {k} T == {p:(aT)| Msize(p) = k } def boolsize size(a)(p) == Msize(x.if p(x) 1 else 0 fi) def sized_bool a {k}  == {p:(a)| size(a)(p) = k } THM card_boolset_vs_mset (a {k} ) ~ (a {k} 2) THM card_st_vs_msize f:(a2). (i:a. P(i)  f(i) = 1  2)  ({x:a| P(x) } ~ (Msize(f))) THM card_st_vs_boolsize p:(a). {x:a| p(x) } ~ (size(a)(p)) THM card_st_sized_bool p:(a {k} ). {i:a| p(i) } ~ k def same_range_sep same_range_sep(A; B) == f,g. j:B. (i:A. f(i) = j)  (i:A. g(i) = j) THM same_range_sep_eqv EquivRel on AB, same_range_sep(A; B) THM same_range_sep_inj_eqv EquivRel on A inj B, same_range_sep(A; B) COM counting_intro2 Counting Indirectly - integer ranges. ... COM counting_intro3 Counting Indirectly - ordered pairs ... COM counting_intro4 Counting Indirectly - tuples ... THM is_list_mem_split x,a:A, ys:A List. (x  a.ys)  x = a  (x  ys) THM is_list_mem_null x:A. (x  nil)  False def list_member_type xs == {a:A| a  xs } THM chessboard_example (AH ~ 8)  ((AH{1...8}) ~ 64) COM counting_intro5 Counting indirectly - dependent ordered pairs ... COM counting_intro6 Counting indirectly - basic forms: dependent pairs (2). Counting(dependent pairs - 1) ...
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html