DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  P  Q == PQ

is mentioned by

Thm*  (AH ~ 8)  ((AH{1...8}) ~ 64)[chessboard_example]
Thm*  x:A. (x  nil)  False[is_list_mem_null]
Thm*  f:(a2). 
Thm*  (i:a. P(i)  f(i) = 1  2)  ({x:a| P(x) } ~ (Msize(f)))		[card_st_vs_msize]
Thm*  ((a onto b))  ba[surj_typing_imp_le]
Thm*  ((a onto b))  ((b inj a))[nsub_surj_imp_a_rev_inj2]
Thm*  e:(BB). 
Thm*  IsEqFun(B;e)
Thm*  
Thm*  (a:, f:(a onto B). (y.least x:. (f(x)) e y)  B inj a)		[nsub_surj_imp_a_rev_inj_gen]
Thm*  Dedekind-Infinite(A)  Finite(A)[dedekind_imp_nonfin]
Thm*  Dedekind-Infinite(A)  Unbounded(A)[dededing_imp_unb_inf]
Thm*  Dedekind-Infinite(A)  Infinite(A)[dedekind_inf_imp_inf]
Thm*  InvFuns(A;A;f;g)  (i:. InvFuns(A;A;f{i};g{i}))[compose_iter_inverses]
Thm*  Bij(A; A; f)  (i:. Bij(A; A; f{i}))[compose_iter_bijection]
Thm*  Surj(A; A; f)  (i:. Surj(A; A; f{i}))[compose_iter_surjection]
Thm*  Inj(A; A; f)  (i:. Inj(A; A; f{i}))[compose_iter_injection]
Thm*  x:A, f:(AA), i,j,k:. k = ij  f{i}{j}(x) = f{k}(x)  A[compose_iter_prod]
Thm*  f:(AA), i,j,k:. k = i+j  f{i} o f{j} = f{k}[compose_iter_sum_comp]
Thm*  x:A, f:(AA), i,j,k:. k = i+j  f{i}(f{j}(x)) = f{k}(x)[compose_iter_sum]
Thm*  f:(AA), u:A. f(u) = u  (i:. f{i}(u) = u)[compose_iter_point_id]
Thm*  a,b:. (A ~ a)  (B ~ b)  ((AB) ~ (ab))[finite_indep_sum_card]
Thm*  a,b,c:. ab = c  ((ab) ~ c)[nsub_mul]
Thm*  c,a,b:. a+b = c    ((a+b) ~ c)[nsub_add]
Thm*  a,b',b:. b = b'+1  ({a...b'} ~ {a..b})[intiseg_intseg]
Thm*  c,a:, b:. c = b-a  ({a..b} ~ c)[nsub_intseg]
Thm*  a,b,a',b':. b-a = b'-a'  ({a..b} ~ {a'..b'})[intseg_shift]
Thm*  a,b:. ba  (Void ~ {a..b})[intseg_void]
Thm*  (A ~ A')  (B ~ B')  ((AB) ~ (A'B'))[function_functionality_wrt_one_one_corr]
Thm*  B,B':(AType). (x:A. B(x) ~ B'(x))  ((x:AB(x)) ~ (x:AB'(x)))[function_functionality_wrt_one_one_corr_B]
Thm*  (x:A. B(x)) ~ (x:A'. B'(x))  ((x:AB(x)) ~ (x:A'B'(x)))[card_pi]
Thm*  a,b:, B:({a..b}Type).
Thm*  a<b  ((i:{a..b}B(i)) ~ ((i:{a..(b-1)}B(i))+B(b-1)))		[card_split_end_sum_intseg_family]
Thm*  (x:A. Dec(P(x)))  (A ~ ({x:A| P(x) }+{x:A| P(x) }))[card_split_decbl_squash]
Thm*  B:(AType), P:(AProp).
Thm*  (i:A. Dec(P(i)))
Thm*  
Thm*  ((i:AB(i)) ~ ((i:{i:A| P(i) }B(i))+(i:{i:A| P(i) }B(i))))		[card_split_sigma_dom_decbl]
Thm*  (x:A. Dec(P(x)))  (A ~ ({x:A| P(x) }+{x:A| P(x) }))[card_split_decbl]
Thm*  (A ~ A')  (B ~ B')  ((AB) ~ (A'B'))[product_functionality_wrt_one_one_corr]
Thm*  B,B':(AType). (x:A. B(x) ~ B'(x))  ((x:AB(x)) ~ (x:AB'(x)))[product_functionality_wrt_one_one_corr_B]
Thm*  (x:A. B(x)) ~ (x:A'. B'(x))  ((x:AB(x)) ~ (x:A'B'(x)))[card_sigma]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } ~ {x:A| B'(x) })[set_functionality_wrt_one_one_corr_n_pred]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } ~ {x:A| B'(x) })[set_functionality_wrt_one_one_corr_n_pred2]
Thm*  Bij(A; A'; f)
Thm*  
Thm*  (x:A. B(x)  B'(f(x)))  ({x:A| B(x) } ~ {x:A'| B'(x) })		[card_settype_sq]
Thm*  Bij(A; A'; f)
Thm*  
Thm*  (x:A. B(x)  B'(f(x)))  ({x:A| B(x) } ~ {x:A'| B'(x) })		[card_settype]
Thm*  (A ~ A')  (B ~ B')  ((A+B) ~ (A'+B'))[union_functionality_wrt_one_one_corr]
Thm*  (A ~ A')  (B ~ B')  (:A. B) ~ (:A'. B')[one_one_corr_fams_indep_if_one_one_corr]
Thm*  g:(A'A). Bij(A'; A; g)  (x:A. B(x)) ~ (x':A'. B(g(x')))[one_one_corr_fams_if_bij_A]
Thm*  (x:A. B(x) ~ B'(x))  (x:A. B(x)) ~ (x:A. B'(x))[one_one_corr_fams_if_one_one_corr_B]
Thm*  f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A;B;f;g))[bij_imp_exists_inv2]
Thm*  P:(ABProp). (x:A. !y:B. P(x;y))  (A ~ (y:B{x:A| P(x;y) }))[partition_type]
Thm*  (A ~ m)  (A ~ k)  m = k[counting_is_unique]
Thm*  (A:Type. Finite(A)  Infinite(A))  (D:Type. (D)  (D))[absurd_nonfinite_imp_infinite]
Thm*  (A:Type. Finite(A)  Unbounded(A))  (P:Prop. P  P)[nonfin_eqv_unb_inf_iff_negnegelim]
Thm*  (A:Type. Finite(A)  Unbounded(A))  (D:Type. (D)  (D))[absurd_nonfin_imp_unb_inf]
Thm*  (P:Prop. P  P)  (A:Type. Finite(A)  Unbounded(A))[negnegelim_imp_notfin_imp_unb_inf]
Thm*  (A ~ B)  Infinite(A)  Infinite(B)[ooc_preserves_infiniteness]
Thm*  (A ~ B)  Unbounded(A)  Unbounded(B)[ooc_preserves_unb_inf]
Thm*  Infinite(A)  Finite(A)[infinite_imp_nonfinite]
Thm*  Unbounded(A)  Finite(A)[unb_inf_not_fin]
Thm*  f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A;B;f;g))[bij_imp_exists_inv_version2]
Thm*  f:(AB), g:(BA). InvFuns(A;B;f;g)  Bij(A; B; f)[fun_with_inv_is_bij_version2]
Thm*  InvFuns(A;B;f;g)  Bij(B; A; g)[fun_with_inv2_is_bij_rev]
Thm*  InvFuns(A;B;f;g)  Bij(A; B; f)[fun_with_inv2_is_bij]
Thm*  (A  C)  (B  D)  A & B  C & D[parallel_conjunct_imp]
Thm*  g:(BA). Surj(A; B; f)  (x:A. g(f(x)) = x)  (y:B. f(g(y)) = y)[left_inv_of_surj_is_right_inv]
Thm*  InvFuns(A;B;f;g)  InvFuns(A;B;f;h)  g = h[inv_funs_2_unique]
Thm*  (A ~ B)  (B ~ C)  (A ~ C)[one_one_corr_2_transitivity]
Thm*  (A ~ B)  (B ~ A)[one_one_corr_2_inversion]
Thm*  (A ~ A')  (B ~ B')  ((A ~ B)  (A' ~ B'))[one_one_corr_2_functionality_wrt_one_one_corr]
Thm*  (A ~ B)  ((A)  (B))[inhabited_functionality_wrt_one_one_corr]
Thm*  (A ~ B)  (A  B)[iff_weakening_wrt_one_one_corr_2]
Thm*  InvFuns(A;B;f;g)  Surj(B; A; g)[fun_with_inv2_is_surj_rev]
Thm*  (A ~ A')  (B ~ B')  ((A inj B) ~ (A' inj B'))[injection_type_functionality_wrt_ooc]
Thm*  InvFuns(A;B;f;g)  Inj(A; B; f) & Inj(B; A; g)[invfuns_are_inj]
Thm*  (A ~ B)  Dedekind-Infinite(A)  Dedekind-Infinite(B)[ooc_preserves_dededkind_inf]
Thm*  InvFuns(A;B;f;g)  Inj(B; A; g)[fun_with_inv2_is_inj_rev]
Thm*  B:(AType), B':(A'Type).
Thm*  (x:A. B(x)) ~ (x':A'. B'(x'))  (x':A'. B'(x')) ~ (x:A. B(x))		[one_one_corr_fams_sym]
Thm*  (A ~ A')  (B ~ B')  ((A onto B) ~ (A' onto B'))[surjection_type_functionality_wrt_ooc]
Thm*  InvFuns(A;B;f;g)  Surj(A; B; f) & Surj(B; A; g)[invfuns_are_surj]
Thm*  InvFuns(A;B;f;g)  InvFuns(B;A;g;f)[inv_funs_2_sym]
Thm*  k:, B:(kType), Q:(x:kB(x)Prop).
Thm*  (x:k. y:B(x). Q(x;y))  (f:(x:kB(x)). x:k. Q(x;f(x)))		[dep_finite_choice]
Thm*  k:, Q:(kAProp).
Thm*  (x:k. y:A. Q(x;y))  (f:(kA). x:k. Q(x;f(x)))		[finite_choice]
Thm*  (x:A. Dec(P(x)))
Thm*  
Thm*  ((x:AB(x)) ~ ((x:A st P(x)B(x))(x:A st P(x)B(x))))		[card_split_prod_intseg_family_decbl]
Thm*  Bij(A; B; g)  Bij(B; C; f)  Bij(A; C; f o g)[comp_preserves_bij]
Thm*  A:Type, A',A'':Type, B:(AType), B':(A'Type), B'':(A''Type).
Thm*  (x:A. B(x)) ~ (x':A'. B'(x'))
Thm*  
Thm*  (x':A'. B'(x')) ~ (x'':A''. B''(x''))  (x:A. B(x)) ~ (x'':A''. B''(x''))		[one_one_corr_fams_trans]
Thm*  (A ~ A')  (B ~ B')  ((AB) ~ (A'B'))[inv_pair_functionality_wrt_one_one_corr]
Thm*  f:(A onto B), a:. a onto A  (B Discrete)  Surj(A; B; f)[surjection_type_surjection]
Thm*  Surj(A; B; g)  Surj(B; C; f)  Surj(A; C; f o g)[comp_preserves_surj]
Thm*  Inj(A; B; g)  Inj(B; C; f)  Inj(A; C; f o g)[comp_preserves_inj]
Thm*  Infinite(A)  Unbounded(A)[unboundedly_imp_productively_infinite]
Thm*  k,n:. k = n+1  k! = kn!  [factorial_via_intseg_step]
Thm*  P:{P:(Prop)| i:. P(i) }. 
Thm*  (i:. Dec(P(i)))  ({i:| P(i) & (j:. j<i  P(j)) })		[least_exists2]
Thm*  k:, P:{P:(kProp)| i:k. P(i) }.
Thm*  (i:k. Dec(P(i)))  ({i:k| P(i) & (j:i. P(j)) })		[least_exists]
Thm*  a,a':. a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a))[card_sum_family_intseg_singleton_elim]
Thm*  A = B  (A ~ B)[one_one_corr_2_weakening_wrt]
Thm*  a,a':. a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a))[card_prod_family_intseg_singleton_elim]
Thm*  k:, j:k, m:. m = k-1  ({i:k| i = j } ~ m)[nsub_delete]
Thm*  a,a':.
Thm*  a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) ~ ({a:}B(a)))		[card_sum_family_singleton_vs_intseg]
Thm*  R:(AAProp). 
Thm*  (A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y))
Thm*  
Thm*  (k:. f:(kA). i,j:k. i<j  R(f(i);f(j)))		[no_finite_model_lemma]
Thm*  (A ~ B)  Finite(A)  Finite(B)[ooc_preserves_finiteness]
Thm*  e:(BB). 
Thm*  IsEqFun(B;e)  (a:, f:(a onto B), y:B. f(least x:. (f(x)) e y) = y)		[nsub_surj_least_preimage_works_gen]
Thm*  e:(BB). 
Thm*  IsEqFun(B;e)  (a:, f:(a onto B), y:B. (least x:. (f(x)) e y)  a)		[nsub_surj_least_preimage_total_gen]
Thm*  (A Discrete)  (k:, f:(k inj A). f  k bij {a:A| i:k. a = f(i) })[nsub_inj_discr_range_bijtype]
Thm*  (A Discrete)
Thm*  
Thm*  (k:, f:(k inj A).
Thm*  ({a:A| i:k. a = f(i) }  Type
Thm*  (& f  k{a:A| i:k. a = f(i) }
Thm*  (& Bij(k; {a:A| i:k. a = f(i) }; f))		[nsub_inj_discr_range_bij]
Thm*  (A Discrete)  (k:, f:(kA). f  k onto {a:A| i:k. a = f(i) })[nsub_discr_range_surjtype]
Thm*  (A Discrete)
Thm*  
Thm*  (k:, f:(kA).
Thm*  ({a:A| i:k. a = f(i) }  Type
Thm*  (& f  k{a:A| i:k. a = f(i) }
Thm*  (& Surj(k; {a:A| i:k. a = f(i) }; f))		[nsub_discr_range_surj]
Thm*  p:{p:()| i:. p(i) }. 
Thm*  (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }		[least_characterized2]
Thm*  InvFuns(A;B;f;g)  Surj(A; B; f)[fun_with_inv2_is_surj]
Thm*  InvFuns(A;B;f;g)  Inj(A; B; f)[fun_with_inv2_is_inj]
Thm*  A = A'  B = B'  (A ~ B) = (A' ~ B')[one_one_corr_2_functionality_wrt_eq]
Thm*  m,k:, f:(mk). k<m  (x,y:m. x  y & f(x) = f(y))[pigeon_hole]
Thm*  m,k:, f:(mk). Inj(m; k; f)  mk[inj_imp_le2]
Thm*  ((m inj k))  mk[inj_typing_imp_le]
Thm*  (f:(mk). Inj(m; k; f))  mk[inj_imp_le]
Thm*  m:, f:(m). Inj(m; ; f)  (x:m, y:x. f(x) = f(y))[finite_inj_counter_example]
Thm*  Bij((m+1); (k+1); f)  Bij(m; k; Replace value k by f(m) in f)[delete_fenum_value_is_fenum]
Thm*  Inj((m+1); (k+1); f)  Inj(m; k; Replace value k by f(m) in f)[delete_fenum_value_is_inj]
Thm*  Inj((m+1); (k+1); f)
Thm*  
Thm*  (i:m. f(i) = k  (Replace value k by f(m) in f)(i) = f(i) k)		[delete_fenum_value_comp2]
Thm*  Inj((m+1); (k+1); f)
Thm*  
Thm*  (i:m. f(i) = k  (Replace value k by f(m) in f)(i) = f(m) k)		[delete_fenum_value_comp1]
Thm*  Inj((m+1); (k+1); f)  (Replace value k by f(m) in f)  mk[delete_fenum_value_wf]
Thm*  Bij({u:| P(u) }; {v:| Q(v) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm*  (Bij({u:| P(u) & u = m }; {v:| Q(v) & v = k };
Thm*  (Bij(Replace value k by f(m) in f))		[delete_fenum_value_is_fenum_gen]
Thm*  Inj({u:| P(u) }; {v:| Q(v) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm*  (Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
Thm*  (Inj(Replace value k by f(m) in f))		[delete_fenum_value_is_inj_gen]
Thm*  Inj({u:| P(u) }; {v:| Q(v) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm*  ((Replace value k by f(m) in f)
Thm*  ( {u:| P(u) & u = m }{v:| Q(v) & v = k }
Thm*  (& Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
Thm*  (& Inj(Replace value k by f(m) in f))		[delete_fenum_value_is_inj_genW]
Thm*  Inj({u:| P(u) }; {u:| Q(u) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }, i:{u:| P(u) & u = m }.
Thm*  (f(i) = k
Thm*  (
Thm*  ((Replace value k by f(m) in f)(i) = f(i)  {v:| Q(v) & v = k })		[delete_fenum_value_comp2_gen]
Thm*  Inj({u:| P(u) }; {u:| Q(u) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }, i:{u:| P(u) & u = m }.
Thm*  (f(i) = k
Thm*  (
Thm*  ((Replace value k by f(m) in f)(i) = f(m)  {v:| Q(v) & v = k })		[delete_fenum_value_comp1_gen]
Thm*  Inj({k:| P(k) }; {k:| Q(k) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm*  ((Replace value k by f(m) in f)
Thm*  ( {u:| P(u) & u = m }{v:| Q(v) & v = k })		[delete_fenum_value_wf_gen]
Thm*  (A)  (!(A inj B))[inj_from_empty_unique]
Thm*  a,a':.
Thm*  a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a)))		[exteq_sum_family_singleton_vs_intseg]
Thm*  a,a':.
Thm*  a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a)))		[exteq_prod_family_singleton_vs_intseg]
Thm*  a,a':. a'-a = 1  ({a..a'} =ext {a:})[exteq_singleton_vs_intseg]
Thm*  a,b:. ab  (b -- a) = b-a[ndiff_vs_diff]
Def  1-1 xA,yB. R(x;y)
Def  == x,x':A, y,y':B. R(x;y) & R(x';y')  (x = x'  y = y')		[rel_1_1_b]
Def  R is 1-1 == x,x':A, y,y':B. R(x,y) & R(x',y')  (x = x'  y = y')[rel_1_1]

In prior sections: core well fnd int 1 bool 1 rel 1 quot 1 LogicSupplement int 2 union num thy 1 SimpleMulFacts IteratedBinops

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

DiscreteMath Sections DiscrMathExt Doc