Nuprl - Pf surj_is_inj

PrintForm Definitions automata 5 Sections AutomataTheory Doc

1. A: Type
2. B: Type
3. f: AB
4. f1: AB
5. g: BA
6. InvFuns(A; B; f1; g)
7. n:
8. f2: nB
9. g1: Bn
10. InvFuns(n; B; f2; g1)
11. Surj(A; B; f)

Inj(A; B; f)

By: Inst Thm* n:, f:(nn). Surj(n; n; f) Inj(n; n; f) [n;g1 o f o g o f2]

Generated subgoals:

1 Surj(n; n; g1 o f o g o f2)

2 12. Inj(n; n; g1 o f o g o f2)
Inj(A; B; f)

About:

1	`Surj(n; n; g1 o f o g o f2)`
2	12. `Inj(n; n; g1 o f o g o f2)` `Inj(A; B; f)`