DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def   == {i:| 0i }

is mentioned by

Thm*  p:(a {k} ). {i:a| p(i) } ~ k[card_st_sized_bool]
Thm*  p:(a). {x:a| p(x) } ~ (size(a)(p))[card_st_vs_boolsize]
Thm*  f:(a2). 
Thm*  (i:a. P(i)  f(i) = 1  2)  ({x:a| P(x) } ~ (Msize(f)))		[card_st_vs_msize]
Thm*  (a {k} ) ~ (a {k} 2)[card_boolset_vs_mset]
Thm*  a,k:. a {k}   Type[sized_bool_wf]
Thm*  a:. size(a)  (a)[boolsize_wf]
Thm*  a,k,x:. a {k} {x...}  Type[sized_mset_wf5]
Thm*  a,k:. a {k}   Type[sized_mset_wf4]
Thm*  a,k,x:, y:. a {k} {x...y}  Type[sized_mset_wf3]
Thm*  a,k,x:, y:. a {k} {x..y}  Type[sized_mset_wf2]
Thm*  a,k:. a {k}   Type[sized_mset_wf]
Thm*  k:. Msize  (k)[msize_wf]
Thm*  (a bij a) ~ (aa)[nsub_bij_ooc_invpair]
Thm*  (k inj k) ~ (k onto k)[nsub_inj_ooc_nsub_surj]
Thm*  (k inj k) ~ (k bij k)[nsub_inj_ooc_nsub_bij]
Thm*  (k inj k) =ext (k bij k)[nsub_inj_exteq_nsub_bij]
Thm*  (k onto k) ~ (k bij k)[nsub_surj_ooc_nsub_bij]
Thm*  (k onto k) =ext (k bij k)[nsub_surj_exteq_nsub_bij]
Thm*  (k inj k) =ext (k onto k)[nsub_inj_exteq_nsub_surj]
Thm*  ((a onto b))  ba[surj_typing_imp_le]
Thm*  ((a onto b))  ((b inj a))[nsub_surj_imp_a_rev_inj2]
Thm*  f:(a bij a). InvFuns(a;a;f;y.least x:. f(x)=y)[nsub_bij_least_preimage_inverse]
Thm*  f:(a onto b). (y.least x:. f(x)=y)  b inj a[nsub_surj_imp_a_rev_inj]
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*  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*  f:(A inj A), i:. f{i}  A inj A[compose_iter_injection2]
Thm*  k:, f:(k inj k). i:. f{i} = Id  kk[iter_perm_cycles_uniform2]
Thm*  k:, f:(k inj k). i:. u:k. f{i}(u) = u[iter_perm_cycles_uniform]
Thm*  k:, f:(k inj k), u:k. i:. f{i}(u) = u[compose_iter_inj_cycles]
Thm*  Inj(A; A; f)  (i:. Inj(A; A; f{i}))[compose_iter_injection]
Thm*  x:A, f:(AA), i,j:. f{i}{j}(x) = f{ij}(x)[compose_iter_prod2]
Thm*  x:A, f:(AA), i,j,k:. k = ij  f{i}{j}(x) = f{k}(x)  A[compose_iter_prod]
Thm*  f:(AA), k:, i:{0...k}. f{k} = f{i} o f{k-i}[compose_iter_sum_comp_rw]
Thm*  x:A, f:(AA), k:, i:{0...k}. f{k}(x) = f{i}(f{k-i}(x))[compose_iter_sum_rw]
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*  i:. Id{i} = Id  AA[compose_iter_id]
Thm*  f:(AA), u:A. f(u) = u  (i:. f{i}(u) = u)[compose_iter_point_id]
Thm*  (k:k) ~ [card_nat_vs_nat_tuples_all]
Thm*  (k:k) ~ [card_nat_vs_nat_tuples]
Thm*  k:. (k) ~ [card_nat_vs_nat_tuple]
Thm*  () ~ [card_nat_vs_nat_nat]
Thm*  f:(AA), i:. f{i}  AA[compose_iter_wf]
Thm*  Bij(; ; nat_to_nat_pair)[nat_to_nat_pair_bij]
Thm*  Surj(; ; nat_to_nat_pair)[nat_to_nat_pair_surj]
Thm*  Inj(; ; nat_to_nat_pair)[nat_to_nat_pair_inj]
Thm*  nat_to_nat_pair  [nat_to_nat_pair_wf]
Thm*  InvFuns(;{xy:()| xy = <0,0>   };next_nat_pair;prev_nat_pair)[next_nat_pair_vs_prev_nat_pair]
Thm*  prev_nat_pair  {xy:()| xy = <0,0>   }[prev_nat_pair_wf]
Thm*  Inj(; ; next_nat_pair)[next_nat_pair_inj]
Thm*  xy:(). <0,0> = next_nat_pair(xy)  [next_nat_pair_not_zeroes]
Thm*  next_nat_pair  [next_nat_pair_wf]
Thm*  a:, b:(a). (i:ab(i)) ~ ( i:a. b(i))[card_sigma_vs_nsub_sigma]
Thm*  a,b:. (a+b) ~ (a+b)[nsub_add_rw]
Thm*  a,b,c:. c(ab) = (ca)b[exp_exp_reduce2]
Thm*  a,b,c:. c(ab) = (cb)a[exp_exp_reduce1]
Thm*  a,b:. (ab) ~ (ba)[card_fun_vs_nsub_exp]
Thm*  a:, b:(a). (i:ab(i)) ~ ( i:a. b(i))[card_pi_vs_nsub_pi]
Thm*  (k inj k) ~ (k!)[nsub_inj_factorial]
Thm*  (a inj b) ~ (b!a)[nsub_inj_factorial_tail]
Thm*  (b inj b) ~ (b!)[nsub_inj_factorial2]
Thm*  a,b:. (A ~ a)  (B ~ b)  ((AB) ~ (ab))[finite_indep_sum_card]
Thm*  a,b,c:. a(bc) = (ab)c[mul_assoc_from_cross_assoc]
Thm*  a,b:. (ab) ~ (ab)[nsub_mul_rw]
Thm*  a,b,c:. ab = c  ((ab) ~ c)[nsub_mul]
Thm*  c,a,b:. a+b = c    ((a+b) ~ c)[nsub_add]
Thm*  Finite()[nat_not_finite]
Thm*  a,b:. (a ~ b)  a = b[fin_card_vs_nat_eq]
Thm*  (A ~ m)  (A ~ k)  m = k[counting_is_unique]
Thm*  (() ~ )[not_nat_occ_natfuns]
Thm*  k:. Infinite(k)[nsub_not_infinite]
Thm*   ~ [int_ooc_nat]
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*  f:(a onto b). Surj(a; b; f)[surjection_type_nsub_surjection]
Thm*  f:(A onto B), a:. a onto A  (B Discrete)  Surj(A; B; f)[surjection_type_surjection]
Thm*  a,b:. (a -- b)  [ndiff_wf_nat]
Thm*  k:. k! = k(k-1)!  [factorial_via_intseg_step_rw]
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*  k:, j:k. {i:k| i = j } ~ (k-1)[nsub_delete_rw]
Thm*  k:, j:k, m:. m = k-1  ({i:k| i = j } ~ m)[nsub_delete]
Thm*  k:. Finite(k)[nsub_is_finite]
Thm*   ~ [nat_plus_ooc_nat]
Thm*  k:. (k+) ~ [fin_plus_nat_ooc_nat]
Thm*  f:(a onto b), y:b. f(least x:. f(x)=y) = y[nsub_surj_least_preimage_works]
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*  f:(a onto b), y:b. (least x:. f(x)=y)  a[nsub_surj_least_preimage_total]
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) }. p(least i:. p(i))[least_satisfies2]
Thm*  p:{p:()| i:. p(i) }, j:(least i:. p(i)). p(j)[least_is_least2]
Thm*  k:, p:{p:(k)| i:k. p(i) }, j:(least i:. p(i)). p(j)[least_is_least]
Thm*  k:, p:{p:(k)| i:k. p(i) }. p(least i:. p(i))[least_satisfies]
Thm*  p:{p:()| i:. p(i) }. (least i:. p(i))  [least_wf2]
Thm*  p:{p:()| i:. p(i) }. 
Thm*  (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }		[least_characterized2]
Thm*  k:, p:{p:(k)| i:k. p(i) }. (least i:. p(i))  k[least_wf]
Thm*  k:, p:{p:(k)| i:k. p(i) }.
Thm*  (least i:. p(i))  {i:k| p(i) & (j:i. p(j)) }		[least_characterized]
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*  a:, b:, j:b, f:((a-1) inj {x:b| x = j }).
Thm*  (i.if i=a-1 j else f(i) fi)  a inj b		[nsub_inj_fill_typing]
Thm*  a:, b:, f:(a inj b). f  (a-1) inj {x:b| x = f(a-1) }[nsub_inj_lop_typing]
Thm*  i,j:. Dec(i = j)[decidable__nat_equal]
Thm*  IsEqFun(b;i,j. i=j)[eq_int_is_eq_nsub]
Def  a {k}  == {p:(a)| size(a)(p) = k }[sized_bool]
Def  a {k} T == {p:(aT)| Msize(p) = k }[sized_mset]
Def  Infinite(A) == ( inj A)[productively_infinite]
Def  Unbounded(A) == k:. (k inj A)[unboundedly_infinite]
Def  fin_enum(A) == k:kA[fin_enum]
Def  Finite(A) == n:. A ~ n[is_finite_type]

In prior sections: int 1 bool 1 int 2 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