DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
2
Thm*
Inj(
A
;
A
;
f
)
(
i
:
. Inj(
A
;
A
;
f
{
i
}))
[compose_iter_injection]
cites the following:
1
Thm*
f
:(
A
A
).
f
{
0} = Id
[compose_iter_zero_id]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
(
i:
. Inj(A; A; f{
i}))f:(A
A). f{0} = Id (i:. Inj(A; A; f{i}))f:(AA). f{0} = Id