Def AB == B<A

is mentioned by

Thm* f:(TT), m:(T). Thm* (x:T. m(f(x))m(x) & (m(f(x)) = m(x)  f(x) = x)) Thm*  Thm* (x:T. n:. f(f^n(x)) = f^n(x))	[iteration_terminates]
Thm* n,m:, f:(nm). Inj(n; m; f)  nm	[pigeon-hole]
Thm* k,b:, f:(k). (x:k. bf(x))  bksum(f(x) | x < k)	[sum_lower_bound]
Thm* k,b:, f:(k). (x:k. f(x)b)  sum(f(x) | x < k)bk	[sum_bound]
Thm* k:, f,g:(k). Thm* (x:k. f(x)g(x))  sum(f(x) | x < k)sum(g(x) | x < k)	[sum_le]
Thm* n:, f:(n). (x:n. 0f(x))  0sum(f(x) | x < n)	[non_neg_sum]
Thm* k,m:. (f:(km). Inj(k; m; f))  km	[injection_le]
Thm* k:, f:(k), x:k. increasing(f;k)  f(0)+xf(x)	[increasing_lower_bound]
Thm* k,m:. (f:(km). increasing(f;k))  km	[increasing_le]
Def nondecreasing(f;k) == i:(k-1). f(i)f(i+1)	[nondecreasing]

In prior sections: int 1 bool 1 int 2 list 1 core

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