Nuprl - Pf fin_dec_fin 2 1 2 2 3 1 3 1

PrintForm Definitions finite sets Sections AutomataTheory Doc

1. n:
2. 0 < n
3. T:Type, B:(TProp). (f:((n-1)T), g:(T(n-1)). InvFuns((n-1); T; f; g)) & (t:T. Dec(B(t))) (m:, f:(m{t:T| B(t) }), g:({t:T| B(t) }m). InvFuns(m; {t:T| B(t) }; f; g))
4. T: Type
5. B: TProp
6. f: nT
7. g: Tn
8. g o f = Id
9. f o g = Id
10. t:T. Dec(B(t))
11. f (n-1){t:T| g(t) < n-1 }
12. g {t:T| g(t) < n-1 }(n-1)

g o f = Id

By: Ext

Generated subgoals:

1 13. x: (n-1)
(g o f)(x) = Id(x)

2 3. T:Type{i}, B:(TProp{i}). (f:((n-1)T), g:(T(n-1)). InvFuns((n-1); T; f; g)) & (t:T. Dec(B(t))) (m:, f:(m{t:T| B(t) }), g:({t:T| B(t) }m). InvFuns(m; {t:T| B(t) }; f; g))
4. T: Type{i}
5. B: TProp{i}
6. f: nT
7. g: Tn
8. g o f = Id
9. f o g = Id
10. t:T. Dec(B(t))
11. f (n-1){t:T| g(t) < n-1 }
12. g {t:T| g(t) < n-1 }(n-1)
(n-1) = (n-1)

3 g o f = g o f

4 Id = Id

About:

1	13. `x:` `(n-1)` `(g o f)(x) = Id(x)`
2	3. `T:Type{i}, B:(TProp{i}). (f:((n-1)T), g:(T(n-1)). InvFuns((n-1); T; f; g)) & (t:T. Dec(B(t))) (m:, f:(m{t:T\| B(t) }), g:({t:T\| B(t) }m). InvFuns(m; {t:T\| B(t) }; f; g))` 4. `T:` `Type{i}` 5. `B:` `TProp{i}` 6. `f:` `nT` 7. `g:` `Tn` 8. `g o f = Id` 9. `f o g = Id` 10. `t:T. Dec(B(t))` 11. `f (n-1){t:T\| g(t) < n-1 }` 12. `g {t:T\| g(t) < n-1 }(n-1)` `(n-1) = (n-1)`
3	`g o f = g o f`
4	`Id = Id`