PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
fin
dec
fin
2
1
2
2
3
1
3
2
1.
n:
2.
0 < n
3.
T:Type, B:(T
Prop). (
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:
T
Prop
6.
f:
n
T
7.
g:
T
n
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)
f o g = Id
By:
Ext
Generated subgoals:
1
13.
x:
{t:T| g(t) < n-1 }
(f o g)(x) = Id(x)
2
{t:T| g(t) < n-1 } = {t:T| g(t) < n-1 }
3
f o g = f o g
4
Id = Id
About: