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
Latex:
X (+) Y == lifting-1(\mlambda{}x.(inl x))|X| || lifting-1(\mlambda{}x.(inr x ))|Y|
Date html generated:
2015_07_21-PM-03_03_22
Last ObjectModification:
2012_04_12-PM-06_09_13
Home
Index