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

is mentioned by

Thm*  (AH ~ 8)  ((AH{1...8}) ~ 64)[chessboard_example]
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:. size(a)  (a)[boolsize_wf]
Thm*  a,k,x:, y:. a {k} {x..y}  Type[sized_mset_wf2]
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*  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*  (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*  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:. (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:. (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*  a,b:, c:{a...b}. ({a..c}+{c..b}) ~ {a..b}[intseg_split]
Thm*  a,b:. {a...b} ~ (1+b-a)[nsub_intiseg_rw]
Thm*  a:, b:. {a...b} ~ {a..(b+1)}[intiseg_intseg_plus]
Thm*  a,b',b:. b = b'+1  ({a...b'} ~ {a..b})[intiseg_intseg]
Thm*  a,b:. {a..b} ~ (b-a)[nsub_intseg_rw]
Thm*  c,a:, b:. c = b-a  ({a..b} ~ c)[nsub_intseg]
Thm*   ~ 2[nsub_bool]
Thm*  Unit ~ 1[nsub_unit]
Thm*  a:, b,c:. {a..b} ~ {(a+c)..(b+c)}[intseg_shift_by]
Thm*  a,b,a',b':. b-a = b'-a'  ({a..b} ~ {a'..b'})[intseg_shift]
Thm*  Void ~ 0[nsub_void]
Thm*  a,b:. ba  (Void ~ {a..b})[intseg_void]
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*  a,b:, c:{a...b}, B:({a..b}Type).
Thm*  (i:{a..b}B(i)) ~ ((i:{a..c}B(i))+(i:{c..b}B(i)))		[card_split_sum_intseg_family]
Thm*  (A+0) ~ A[card_nsub0_union_2]
Thm*  (0+A) ~ A[card_nsub0_union]
Thm*  (A+B) ~ (i:2if i=0 A else B fi)[card_union_vs_sigma]
Thm*  InvFuns(A+B;i:2if i=0 A else B fi;union_to_sigma;sigma_to_union)[union_sigma_inverses]
Thm*  a,b:, c:{a...b}, B:({a..b}Type).
Thm*  (i:{a..b}B(i)) ~ ((i:{a..c}B(i))(i:{c..b}B(i)))		[card_split_prod_intseg_family]
Thm*  A:Type, n:, x:A, xs:((n-1)A). [x/ xs]  nA[seq_cons_wf]
Thm*  a,b:. (a ~ b)  a = b[fin_card_vs_nat_eq]
Thm*  (A ~ m)  (A ~ k)  m = k[counting_is_unique]
Thm*  k:. Infinite(k)[nsub_not_infinite]
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:Type. sigma_to_union  (i:2if i=0 A else B fi)(A+B)[sigma_to_union_wf]
Thm*  A,B:Type. union_to_sigma  (A+B)(i:2if i=0 A else B fi)[union_to_sigma_wf]
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*  Dec(P)  (!i:2. if i=0 P else P fi)[decidable_vs_unique_nsub2]
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 ~ 0)  (A)[card0_iff_uninhabited]
Thm*  a,a':. a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a))[card_prod_family_intseg_singleton_elim]
Thm*  a,b:. (a inj b) ~ (b((a-1) inj (b-1)))[card_nsub_inj_vs_lopped]
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*  (0A) ~ 1[card_void_dom_fun_unit]
Thm*  (A ~ 1)  (!A)[card1_iff_inhabited_uniquely]
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*  k:. Finite(k)[nsub_is_finite]
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) }, 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*  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*  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*  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  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 LogicSupplement

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

DiscreteMath Sections DiscrMathExt Doc