Nuprl Definition : eclass-disju
X + Y == (λl,x. (inl x) o X) || (λl,x. (inr x ) o Y)
Definitions occuring in Statement :
parallel-class: X || Y,
eclass1: (f o X),
lambda: λx.A[x],
inr: inr x ,
inl: inl x
FDL editor aliases :
eclass-disju
Latex:
X + Y == (\mlambda{}l,x. (inl x) o X) || (\mlambda{}l,x. (inr x ) o Y)
Date html generated:
2015_07_21-PM-02_37_17
Last ObjectModification:
2012_08_14-PM-11_27_15
Home
Index