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