Nuprl - mb_nat LEMMAs for pair_support_double

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
4	Thm* n,m:, f:(nm), x1,x2:n, y1,y2:m. Thm* x1 = x2 y1 = y2 Thm* Thm* (x:n, y:m. (x = x1 & y = y1) (x = x2 & y = y2) f(x,y) = 0) Thm* Thm* sum(f(x,y) \| x < n; y < m) = f(x1,y1)+f(x2,y2)	[pair_support_double_sum]
cites the following:
3	Thm* n:, f:(n), m,k:n. Thm* m = k Thm* Thm* (x:n. x = m x = k f(x) = 0) sum(f(x) \| x < n) = f(m)+f(k)	[pair_support]
1	Thm* n:, f:(n). (x:n. f(x) = 0) sum(f(x) \| x < n) = 0	[empty_support]
2	Thm* n:, f:(n), m:n. Thm* (x:n. x = m f(x) = 0) sum(f(x) \| x < n) = f(m)	[singleton_support_sum]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html