Nuprl Definition : disjoint-union-comb

X (+) Y == lifting-1(

x.(inl x ))|X| || lifting-1(

x.(inr x ))|Y|

Definitions occuring in Statement : simple-comb-1: F|X|, parallel-class: X || Y, lambda:

x.A[x], inr: inr x , inl: inl x , lifting-1: lifting-1(f)
FDL editor aliases : disjoint-union-comb

X (+) Y == lifting-1(\mlambda{}x.(inl x ))|X| || lifting-1(\mlambda{}x.(inr x ))|Y| Date html generated: 2012_01_23-PM-01_24_57 Last ObjectModification: 2011_12_06-PM-06_28_02 Home Index