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

PrintForm Definitions finite sets Sections AutomataTheory Doc

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

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. 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)

By: Analyze 14 THEN Inst Thm* a:, n:. an (a n) = ((a-n) n)+1 [an+a1;n]

Generated subgoals:

1 14. 0a
15. a < n
16. a-1 = (((a-1)n+a1) n)
0an+a1

2 14. 0a
15. a < n
16. a-1 = (((a-1)n+a1) n)
an+a1n

About:

1	14. `0a` 15. `a < n` 16. `a-1 = (((a-1)n+a1) n)` `0an+a1`
2	14. `0a` 15. `a < n` 16. `a-1 = (((a-1)n+a1) n)` `an+a1n`