Nuprl - Pf prod_fin_is_fin 1 2 6 2 1 1 1 3 1 1 1

PrintForm Definitions finite sets Sections AutomataTheory Doc

At: prod fin is fin 1 2 6 2 1 1 1 3 1 1 1

1. T: Type
2. t: T
3. n:
4. f: nT
5. Inj(n; T; f)
6. b:T. a:n. f(a) = b
7. n > 0
8. b1: T
9. b2: T
10. a: n
11. f(a) = b1
12. a1: n
13. f(a1) = b2

a = ((an+a1) n)

By: Thin 11 THEN Analyze 10 THEN IntInd 10

Generated subgoals:

1 10. a1: n
11. f(a1) = b2
12. 00
13. 0 < n
0 = ((0n+a1) n)

2 10. a1: n
11. f(a1) = b2
12. a:
13. 0 < a
14. 0 a-1 < n a-1 = (((a-1)n+a1) n)
15. 0a
16. a < n
a = ((an+a1) n)

About:

1	10. `a1:` `n` 11. `f(a1) = b2` 12. `00` 13. `0 < n` `0 = ((0n+a1) n)`
2	10. `a1:` `n` 11. `f(a1) = b2` 12. `a:` 13. `0 < a` 14. `0 a-1 < n a-1 = (((a-1)n+a1) n)` 15. `0a` 16. `a < n` `a = ((an+a1) n)`