IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  AB == B<A

is mentioned by

Thm*  a,b:, e:({a..b}). ba  ( i:{a..b}. e(i)) = 0[sum_via_intseg_null]
Thm*  a,b:, e:({a..b}). ba  ( i:{a..b}. e(i)) = 1[mul_via_intseg_null]
Thm*  m,k:. mk  k!m = ((k!)  ((k-m)!))[factorial_ratio2]
Thm*  m,k:. mk  k! = (k-m)!k!m[factorial_ratio]
Thm*  n,m,k:. nk-m  mk  k!(n+m) = (k-m)!nk!m[factorial_tail_split_mid]
Thm*  a,b:, P:({a..b}Prop). ba  (i:{a..b}. P(i))[exist_intseg_null]
Thm*  a,c,b:, e:({a..b}).
Thm*  ac
Thm*  
Thm*  cb  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))( i:{c..b}. e(i))		[mul_via_intseg_split_mid]
Thm*  a,c,b:, e:({a..b}).
Thm*  ac
Thm*  
Thm*  cb  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))+( i:{c..b}. e(i))		[sum_via_intseg_split_mid]
Thm*  a,c,b:, e:({a..b}).
Thm*  ac
Thm*  
Thm*  c<b
Thm*  
Thm*  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c)( i:{c+1..b}. e(i))		[mul_via_intseg_split_pluck]
Thm*  a,c,b:, e:({a..b}).
Thm*  ac
Thm*  
Thm*  c<b
Thm*  
Thm*  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))+e(c)+( i:{c+1..b}. e(i))		[sum_via_intseg_split_pluck]
Thm*  f:(AAA), u:A.
Thm*  is_ident(A; f; u)
Thm*  
Thm*  is_assoc_sep(A; f)
Thm*  
Thm*  (a,c,b:, e:({a..b}A).
Thm*  (ac
Thm*  (
Thm*  (c<b
Thm*  (
Thm*  ((Iter(f;u) i:{a..b}. e(i))
Thm*  (=
Thm*  (f((Iter(f;u) i:{a..c}. e(i)),f(e(c),Iter(f;u) i:{c+1..b}. e(i))))		[iter_via_intseg_split_pluck]
Thm*  f:(AAA), u:A.
Thm*  is_ident(A; f; u)
Thm*  
Thm*  is_assoc_sep(A; f)
Thm*  
Thm*  (a,b:, c:{a...b}, d:{c..b}, e:({a..b}A).
Thm*  ((i:{a..b}. i<c  di  e(i) = u)
Thm*  (
Thm*  ((Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) i:{c..d}. e(i)))		[iter_via_intseg_amputate_units]
Thm*  f:(AAA), u:A.
Thm*  is_ident(A; f; u)
Thm*  
Thm*  is_assoc_sep(A; f)
Thm*  
Thm*  (a,c,b:, e:({a..b}A).
Thm*  (ac
Thm*  (
Thm*  (cb
Thm*  (
Thm*  ((Iter(f;u) i:{a..b}. e(i))
Thm*  (=
Thm*  (f((Iter(f;u) i:{a..c}. e(i)),Iter(f;u) i:{c..b}. e(i)))		[iter_via_intseg_split_mid]
Thm*  f:(AAA), u:A, a,b:, e:({a..b}A).
Thm*  ba  (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) i:{a..a}. e(i))		[iter_via_intseg_nullnorm]
Thm*  f:(AAA), u:A, a,b:, e:({a..b}A).
Thm*  ba  (Iter(f;u) i:{a..b}. e(i)) = u		[iter_via_intseg_null]

In prior sections: int 1 bool 1 int 2 num thy 1 SimpleMulFacts core

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

IteratedBinops Sections DiscrMathExt Doc