Nuprl - Pf fun_preserves_fin 1 1 1 1 1 1 1 1 1 1 1

PrintForm Definitions exponent Sections AutomataTheory Doc

At: fun preserves fin 1 1 1 1 1 1 1 1 1 1 1

1. S: Type
2. T: Type
3. n:
4. f: nS
5. g: Sn
6. g o f = Id & f o g = Id
7. n1:
8. f1: n1T
9. g1: Tn1
10. g1 o f1 = Id & f1 o g1 = Id
11. f:((nn1)(n1n)), g:((n1n)nn1). InvFuns(nn1; (n1n); f; g)

n:, f:(nST), g:((ST)n). g o f = Id & f o g = Id (ST)ST

By: Unfold `inv_funs` 11

Generated subgoal:

1 11. f:((nn1)(n1n)), g:((n1n)nn1). g o f = Id (nn1)nn1 & f o g = Id (n1n)(n1n)
n:, f:(nST), g:((ST)n). g o f = Id & f o g = Id (ST)ST

About: