Def  {i...j} == {k:| ik & kj }

is mentioned by

Thm*  (AH ~ 8)  ((AH{1...8}) ~ 64)	[chessboard_example]
Thm*  a,k,x:, y:. a {k} {x...y}  Type	[sized_mset_wf3]
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*  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:, 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,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]

In prior sections: int 1 IteratedBinops

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