WhoCites
Definitions
DiscrMathExt
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Diagonalization
Who Cites diagonalize?
diagonalize
Def (Diag
f
wrt
y
.
e
(
y
))(
x
) ==
e
(
f
(
x
,
x
))
Thm*
B
:Type,
e
:(
B
B
),
A
:Type,
f
:(
A
A
B
). (Diag
f
wrt
y
.
e
(
y
))
A
B
Syntax:
Diag
f
wrt
y
.
e
(
y
)
has structure:
diagonalize(
y
.
e
(
y
);
f
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
DiscrMathExt
Sections
NuprlLIB
Doc
B:Type, e:(B
B), A:Type, f:(AAB). (Diag f wrt y. e(y)) 
ABB:Type, e:(BB), A:Type, f:(AAB). (Diag f wrt y. e(y)) AB
