Def  AB == B<A

is mentioned by

Thm*  k:{2...}, n:, g:({2..k}). Thm*  2  n < k+1 Thm*   Thm*  (i:{2..k}. ni  0<g(i)  prime(i)) Thm*   Thm*  (h:({2..k}).  Thm*  ({2..k}(g) = {2..k}(h) & is_prime_factorization(2; k; h))	[prime_factorization_existsLEMMA]
Thm*  a,b:, f:({a..b}). ba  {a..b}(f) = {a..a}(f)	[eval_factorization_nullnorm]
Thm*  a,b:, f:({a..b}). ba  {a..b}(f) = 1	[eval_factorization_intseg_null]
Thm*  a:, b:, f:({a..b}), j:{a..b}. Thm*  2j  0<f(j)  {a..b}(reduce_factorization(f; j))<{a..b}(f)	[eval_reduce_factorization_less]
Thm*  a,b:, f:({a..b}), j:{a..b}. Thm*  0<f(j)  (i:{a..b}. reduce_factorization(f; j)(i)f(i))	[reduce_factorization_bound]
Thm*  a,c,b:, f:({a..b}). Thm*  ac  c<b  {a..b}(f) = {a..c}(f)cf(c){c+1..b}(f)	[eval_factorization_split_pluck]
Thm*  a,c,b:, f:({a..b}). Thm*  ac  cb  {a..b}(f) = {a..c}(f){c..b}(f)	[eval_factorization_split_mid]
Thm*  a,b:, P:({a..b}Prop), n:{(a+1)..(b+1)}. Thm*  P(n-1)  (i:{a..b}. ni  P(i))  (i:{a..b}. n-1i  P(i))	[extend_intseg_upperpart_down]

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

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