a,b:
, f:({a..b
}
). is_prime_factorization(a; b; f) 
Propf:(Prime), k:. f is a factorization of k Propa,b:, P:({a..b}Prop), n:{(a+1)..(b+1)}.
Thm* P(n-1)
(i:{a..b}. n
i P(i)) (i:{a..b}. n-1i P(i))is mentioned by
| a,b:, f:({a..b}). is_prime_factorization(a; b; f) Prop | [is_prime_factorization_wf] |
| f:(Prime), k:. f is a factorization of k Prop | [prime_factorization_of_wf] |
| 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: core well fnd int 1 bool 1 rel 1 quot 1 LogicSupplement int 2 IteratedBinops
Try larger context:
DiscrMathExt
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html