(7steps total)
PfGloss
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The range of a finite injection is as big as its domain.
At:
inj
imp
le
m
,
k
:
. (
f
:(
m
k
). Inj(
m
;
k
;
f
))
m
k
By:
Induction on
m
, with trivial base case
0
k
Generated subgoal:
1
1.
m
:
2. 0<
m
3.
k'
:
. (
f'
:(
(
m
-1)
k'
). Inj(
(
m
-1);
k'
;
f'
))
m
-1
k'
4.
k
:
5.
f
:(
m
k
). Inj(
m
;
k
;
f
)
m
k
6
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PfGloss
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
m,k:
. (
f:(m
k). Inj(m; k; f)) 
m
k m,k:. (f:(mk). Inj(m; k; f)) mkk
k':. (f':((m-1)k'). Inj((m-1); k'; f')) m-1k'
f:(mk). Inj(m; k; f)
mk
