Nuprl - Pf prod_fin_is

PrintForm Definitions finite sets Sections AutomataTheory Doc

1. T: Type
2. t: T
3. n:
4. f: nT
5. Bij(n; T; f)
6. n > 0

Bij((nn); TT; x. < f(x n),f(x rem n) > )

By: Analyze 5 THEN Analyze 0

Generated subgoals:

1 5. Inj(n; T; f)
6. Surj(n; T; f)
7. n > 0
Inj((nn); TT; x. < f(x n),f(x rem n) > )

2 5. Inj(n; T; f)
6. Surj(n; T; f)
7. n > 0
Surj((nn); TT; x. < f(x n),f(x rem n) > )

About:

1	5. `Inj(n; T; f)` 6. `Surj(n; T; f)` 7. `n > 0` `Inj((nn); TT; x. < f(x n),f(x rem n) > )`
2	5. `Inj(n; T; f)` 6. `Surj(n; T; f)` 7. `n > 0` `Surj((nn); TT; x. < f(x n),f(x rem n) > )`