Nuprl - DiscreteMath Citations of union_to

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def union_to_sigma(e) == InjCase(e; a. <0,a>; b. <1,b>)

is mentioned by

Thm* InvFuns(A+B;i:2if i=0 A else B fi;union_to_sigma;sigma_to_union) [union_sigma_inverses]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html