Def  least i:. p(i) == if p(0) 0 else (least i:. p(i+1))+1 fi  (recursive)

is mentioned by

Thm*  f:(a bij a). InvFuns(a;a;f;y.least x:. f(x)=y)	[nsub_bij_least_preimage_inverse]
Thm*  f:(a onto b). (y.least x:. f(x)=y)  b inj a	[nsub_surj_imp_a_rev_inj]
Thm*  e:(BB).  Thm*  IsEqFun(B;e) Thm*   Thm*  (a:, f:(a onto B). (y.least x:. (f(x)) e y)  B inj a)	[nsub_surj_imp_a_rev_inj_gen]
Thm*  f:(a onto b), y:b. f(least x:. f(x)=y) = y	[nsub_surj_least_preimage_works]
Thm*  e:(BB).  Thm*  IsEqFun(B;e)  (a:, f:(a onto B), y:B. f(least x:. (f(x)) e y) = y)	[nsub_surj_least_preimage_works_gen]
Thm*  f:(a onto b), y:b. (least x:. f(x)=y)  a	[nsub_surj_least_preimage_total]
Thm*  e:(BB).  Thm*  IsEqFun(B;e)  (a:, f:(a onto B), y:B. (least x:. (f(x)) e y)  a)	[nsub_surj_least_preimage_total_gen]
Thm*  p:{p:()| i:. p(i) }. p(least i:. p(i))	[least_satisfies2]
Thm*  p:{p:()| i:. p(i) }, j:(least i:. p(i)). p(j)	[least_is_least2]
Thm*  k:, p:{p:(k)| i:k. p(i) }, j:(least i:. p(i)). p(j)	[least_is_least]
Thm*  k:, p:{p:(k)| i:k. p(i) }. p(least i:. p(i))	[least_satisfies]
Thm*  p:{p:()| i:. p(i) }.  Thm*  (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }	[least_characterized2]
Thm*  k:, p:{p:(k)| i:k. p(i) }. Thm*  (least i:. p(i))  {i:k| p(i) & (j:i. p(j)) }	[least_characterized]

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