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:ap(i) } ~ k[card_st_sized_bool]
Thm*  p:(a). {x:ap(x) } ~ (size(a)(p))[card_st_vs_boolsize]
Thm*  f:(a2). 
Thm*  (i:aP(i f(i) = 1  2)  ({x:aP(x) } ~ (Msize(f)))
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*  (a:f:(a onto B). (y.least x:. (f(x)) e y B inj a)
Thm*  k:f:(k inj k). i:f{i} = Id  kk[iter_perm_cycles_uniform2]
Thm*  k:f:(k inj k). i:u:kf{i}(u) = u[iter_perm_cycles_uniform]
Thm*  k:f:(k inj k), u:ki: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:ab(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:ab(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)))
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)))
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)))
Thm*  A:Type, n:x:Axs:((n-1)A). [xxs 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:ky:B(x). Q(x;y))  (f:(x:kB(x)). x:kQ(x;f(x)))
Thm*  k:Q:(kAProp).
Thm*  (x:ky:AQ(x;y))  (f:(kA). x:kQ(x;f(x)))
Thm*  f:(a onto b). Surj(abf)[surjection_type_nsub_surjection]
Thm*  f:(A onto B), a:a onto A  (B Discrete)  Surj(ABf)[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:kP(i) }.
Thm*  (i:k. Dec(P(i)))  ({i:kP(i) & (j:iP(j)) })
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:ki = j } ~ (k-1)[nsub_delete_rw]
Thm*  k:j:km:m = k-1  ({i:ki = 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)))
Thm*  R:(AAProp). 
Thm*  (A) & (Trans x,y:AR(x;y)) & (x:Ay:AR(x;y))
Thm*  (k:f:(kA). i,j:ki<j  R(f(i);f(j)))
Thm*  k:. Finite(k)[nsub_is_finite]
Thm*  k:. (k+) ~ [fin_plus_nat_ooc_nat]
Thm*  f:(a onto b), y:bf(least x:f(x)=y) = y[nsub_surj_least_preimage_works]
Thm*  e:(BB). 
Thm*  IsEqFun(B;e (a:f:(a onto B), y:Bf(least x:. (f(x)) e y) = y)
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)
Thm*  (A Discrete)  (k:f:(k inj A). f  k bij {a:Ai:ka = f(i) })[nsub_inj_discr_range_bijtype]
Thm*  (A Discrete)
Thm*  (k:f:(k inj A).
Thm*  ({a:Ai:ka = f(i) }  Type
Thm*  (f  k{a:Ai:ka = f(i) }
Thm*  (& Bij(k; {a:Ai:ka = f(i) }; f))
Thm*  (A Discrete)  (k:f:(kA). f  k onto {a:Ai:ka = f(i) })[nsub_discr_range_surjtype]
Thm*  (A Discrete)
Thm*  (k:f:(kA).
Thm*  ({a:Ai:ka = f(i) }  Type
Thm*  (f  k{a:Ai:ka = f(i) }
Thm*  (& Surj(k; {a:Ai:ka = f(i) }; f))
Thm*  p:{p:()| i:p(i) }, j:(least i:p(i)). p(j)[least_is_least2]
Thm*  k:p:{p:(k)| i:kp(i) }, j:(least i:p(i)). p(j)[least_is_least]
Thm*  k:p:{p:(k)| i:kp(i) }. p(least i:p(i))[least_satisfies]
Thm*  k:p:{p:(k)| i:kp(i) }. (least i:p(i))  k[least_wf]
Thm*  k:p:{p:(k)| i:kp(i) }.
Thm*  (least i:p(i))  {i:kp(i) & (j:ip(j)) }
Thm*  m,k:f:(mk). k<m  (x,y:mx  y & f(x) = f(y))[pigeon_hole]
Thm*  m,k:f:(mk). Inj(mkf mk[inj_imp_le2]
Thm*  ((m inj k))  mk[inj_typing_imp_le]
Thm*  (f:(mk). Inj(mkf))  mk[inj_imp_le]
Thm*  m:f:(m). Inj(mf (x:my:xf(x) = f(y))[finite_inj_counter_example]
Thm*  Bij((m+1); (k+1); f Bij(mk; Replace value k by f(m) in f)[delete_fenum_value_is_fenum]
Thm*  Inj((m+1); (k+1); f Inj(mk; Replace value k by f(m) in f)[delete_fenum_value_is_inj]
Thm*  Inj((m+1); (k+1); f)
Thm*  (i:mf(i) = k  (Replace value k by f(m) in f)(i) = f(ik)
Thm*  Inj((m+1); (k+1); f)
Thm*  (i:mf(i) = k  (Replace value k by f(m) in f)(i) = f(mk)
Thm*  Inj((m+1); (k+1); f (Replace value k by f(m) in f mk[delete_fenum_value_wf]
Thm*  a:b:j:bf:((a-1) inj {x:bx = j }).
Thm*  (i.if i=a-1 j else f(i) fi)  a inj b
Thm*  a:b:f:(a inj b). f  (a-1) inj {x:bx = 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)))
Thm*  a,a':.
Thm*  a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a)))
Thm*  a,a':a'-a = 1  ({a..a'} =ext {a:})[exteq_singleton_vs_intseg]
Thm*  IsEqFun(b;i,ji=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