Nuprl - Pf surj_is_inj_gen 1 1 1 1 2 1 1 1 1 2 1 1 1 1 1

PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: surj is inj gen 1 1 1 1 2 1 1 1 1 2 1 1 1 1 1

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. g1 o f2 = Id
11. f2 o g1 = Id
12. Surj(A; B; f)
13. a1: A
14. a2: A
15. f(a1) = f(a2)
16. g1(f1(a1)) = g1(f1(a2))
17. f1(a1) = f1(a2)
18. (g o f1)(a1) = (g o f1)(a2)

a1 = a2

By: Analyze 6

Generated subgoal:

1 6. g o f1 = Id
7. f1 o g = Id
8. n:
9. f2: nB
10. g1: Bn
11. g1 o f2 = Id
12. f2 o g1 = Id
13. Surj(A; B; f)
14. a1: A
15. a2: A
16. f(a1) = f(a2)
17. g1(f1(a1)) = g1(f1(a2))
18. f1(a1) = f1(a2)
19. (g o f1)(a1) = (g o f1)(a2)
a1 = a2

About: