Nuprl Definition : b-union

The union of two types is special case of the union of family of types,
where we use the booleans to index the family.⋅

A ⋃ ==  ⋃x:𝔹.if then else fi 

Definitions occuring in Statement :  ifthenelse: if then else fi  bool: 𝔹 tunion: x:A.B[x]
Definitions occuring in definition :  tunion: x:A.B[x] bool: 𝔹 ifthenelse: if then else fi 
Rules referencing :  StrongContinuity2
FDL editor aliases :  b-union

A  \mcup{}  B  ==    \mcup{}x:\mBbbB{}.if  x  then  A  else  B  fi 

Date html generated: 2016_07_08-PM-04_46_48
Last ObjectModification: 2015_09_22-PM-05_44_33

Theory : union

Home Index