(4steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
flip
bijection
k
:
,
i
,
j
:
k
. Bij(
k
;
k
; (
i
,
j
))
By:
Unfold `biject` 0 THEN Unfolds [`inject`;`surject`] 0
Generated subgoals:
1
1.
k
:
2.
i
:
k
3.
j
:
k
4.
a1
:
k
5.
a2
:
k
6. (
i
,
j
)(
a1
) = (
i
,
j
)(
a2
)
a1
=
a2
1
step
2
1.
k
:
2.
i
:
k
3.
j
:
k
4.
b
:
k
a
:
k
. (
i
,
j
)(
a
) =
b
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
k:
, i,j:k. Bij(k; k; (i, j)) k:, i,j:k. Bij(k; k; (i, j))
k
k
k
k
a1 = a2
k
k
k
a:k. (i, j)(a) = b
