Nuprl Definition : unit-prod
I x (X;d) == prod-metric-space(2;λi.if (i =z 0) then I else <X, d> fi )
Definitions occuring in Statement :
unit-interval-ms: I,
prod-metric-space: prod-metric-space(k;X),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
lambda: λx.A[x],
pair: <a, b>,
natural_number: $n
Definitions occuring in definition :
prod-metric-space: prod-metric-space(k;X),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
natural_number: $n,
unit-interval-ms: I,
pair: <a, b>
FDL editor aliases :
unit-prod
Latex:
I x (X;d) == prod-metric-space(2;\mlambda{}i.if (i =\msubz{} 0) then I else <X, d> fi )
Date html generated:
2019_10_29-AM-11_13_57
Last ObjectModification:
2019_10_02-AM-09_54_12
Theory : reals
Home
Index