Nuprl Definition : per-or-family
per-or-family(A;B) ==  λx.if x = Ax then A otherwise B
Definitions occuring in Statement : 
isaxiom: if z = Ax then a otherwise b
, 
lambda: λx.A[x]
Definitions occuring in definition : 
lambda: λx.A[x]
, 
isaxiom: if z = Ax then a otherwise b
FDL editor aliases : 
per-or-family
Latex:
per-or-family(A;B)  ==    \mlambda{}x.if  x  =  Ax  then  A  otherwise  B
Date html generated:
2019_06_20-AM-11_30_00
Last ObjectModification:
2018_08_22-PM-01_59_43
Theory : per!type
Home
Index