Nuprl - FTA Citations of lelt

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

j < k == i

j & j<k

is mentioned by

Thm*  a,b:, f:({a..b}), x:.
Thm*  a  x < b  complete_intseg_mset(a; b; f)(x) = 0 [complete_intseg_mset_ismin]

Thm*  i,j,k:. i  j < k  i  j < k [lelt_int_vs_lelt]

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]

In prior sections: int 1 SimpleMulFacts int 2

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

FTA Sections DiscrMathExt Doc

Thm* a,b:, f:({a..b}), x:. Thm* a x < b complete_intseg_mset(a; b; f)(x) = 0	[complete_intseg_mset_ismin]
Thm* i,j,k:. i j < k i j < k	[lelt_int_vs_lelt]
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]