Def  P  Q == (P  Q) & (P  Q)

is mentioned by

Thm*  i,j,k:. i  j < k  i  j < k	[lelt_int_vs_lelt]
Thm*  a:{2...}, b:, f:({a..b}). Thm*  {a..b}(f) = 1  (i:{a..b}. f(i) = 0)	[eval_factorization_not_one]
Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  f = (x.0)	[eval_factorization_one_c]
Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  (i:{a..b}. 0<f(i))	[eval_factorization_one_b]
Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  (i:{a..b}. f(i) = 0)	[eval_factorization_one]

In prior sections: core well fnd int 1 bool 1 rel 1 quot 1 LogicSupplement int 2 num thy 1 SimpleMulFacts IteratedBinops

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