is mentioned by
Thm* (i:m. Dec(P(i))) Thm* Thm* (n,k:, f:(nm), g:(km). Thm* (increasing(f;n) Thm* (& increasing(g;k) Thm* (& (i:n. P(f(i))) Thm* (& (j:k. P(g(j))) Thm* (& (i:m. (j:n. i = f(j)) (j:k. i = g(j)))) | [increasing_split] |
Thm* increasing(f;n) nondecreasing(g;n) increasing(fadd(f;g);n) | [fadd_increasing] |
Thm* increasing(f;n) Thm* Thm* increasing(g;k) Thm* Thm* (i:m. (j:n. i = f(j)) (j:k. i = g(j))) Thm* Thm* (j1:n, j2:k. f(j1) = g(j2)) m = n+k | [disjoint_increasing_onto] |
[increasing_lower_bound] | |
[increasing_is_id] | |
[increasing_le] | |
[increasing_inj] | |
Thm* increasing(f;k) increasing(g;m) increasing(g o f;k) | [compose_increasing] |
[increasing_implies] | |
[id_increasing] |
Try larger context:
MarkB generic
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html