Nuprl Definition : uand
uand(A;B) == ⋂x:Base. ⋂p:(x)↓. if x = Ax then A otherwise B
Definitions occuring in Statement :
has-value: (a)↓,
isaxiom: if z = Ax then a otherwise b,
isect: ⋂x:A. B[x],
base: Base
Definitions occuring in definition :
base: Base,
isect: ⋂x:A. B[x],
has-value: (a)↓,
isaxiom: if z = Ax then a otherwise b
FDL editor aliases :
uand
Latex:
uand(A;B) == \mcap{}x:Base. \mcap{}p:(x)\mdownarrow{}. if x = Ax then A otherwise B
Date html generated:
2016_05_13-PM-03_53_20
Last ObjectModification:
2015_09_22-PM-05_45_30
Theory : per!type
Home
Index