Nuprl Definition : per-or

per-or(A;B) ==  per-exists(per-value();x.if x = Ax then A otherwise B)


Definitions occuring in Statement :  per-value: per-value(),  per-exists: per-exists(A;a.B[a]),  isaxiom: if z = Ax then a otherwise b
Definitions occuring in definition :  per-exists: per-exists(A;a.B[a]),  per-value: per-value(),  isaxiom: if z = Ax then a otherwise b
FDL editor aliases :  per-or
Latex:
per-or(A;B)  ==    per-exists(per-value();x.if  x  =  Ax  then  A  otherwise  B)


Date html generated: 2016_05_13-PM-03_54_38
Last ObjectModification: 2015_09_22-PM-05_45_33

Theory : per!type


Home Index