Nuprl - Pf one2one_preserves_fin 1 1 1 1 1 1 1 1 1 1 1 1 1 2 1 1 1 1 1 1 1

PrintForm Definitions finite sets Sections AutomataTheory Doc

At: one2one preserves fin 1 1 1 1 1 1 1 1 1 1 1 1 1 2 1 1 1 1 1 1 1

1. T: Type
2. U: Type
3. f: TU
4. g: UT
5. g o f = Id
6. f o g = Id
7. n:
8. f1: nT
9. Inj(n; T; f1)
10. b: U
11. a: n
12. f1(a) = g(b)
13. (f o f1)(a) = (f o g)(b)

a:n. (f o f1)(a) = b

By: RWH (HypC 6) 13

Generated subgoal:

1 13. (f o f1)(a) = Id(b)
a:n. (f o f1)(a) = b

About: