Nuprl Definition : union-metric-space
union-metric-space(T;eq;X) ==
i:T × (fst((X i))) with λp,q. let i,v = p in let j,w = q in if eq i j then rmin(mdist(snd((X i));v;w);r1) else r1 fi
Definitions occuring in Statement :
mk-metric-space: X with d,
mdist: mdist(d;x;y),
rmin: rmin(x;y),
int-to-real: r(n),
ifthenelse: if b then t else f fi ,
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
spread: spread def,
product: x:A × B[x],
natural_number: $n
Definitions occuring in definition :
mk-metric-space: X with d,
product: x:A × B[x],
pi1: fst(t),
lambda: λx.A[x],
spread: spread def,
ifthenelse: if b then t else f fi ,
rmin: rmin(x;y),
mdist: mdist(d;x;y),
pi2: snd(t),
apply: f a,
int-to-real: r(n),
natural_number: $n
FDL editor aliases :
union-metric-space
Latex:
union-metric-space(T;eq;X) ==
i:T \mtimes{} (fst((X i))) with \mlambda{}p,q. let i,v = p
in let j,w = q
in if eq i j then rmin(mdist(snd((X i));v;w);r1) else r1 fi
Date html generated:
2019_10_29-AM-11_11_56
Last ObjectModification:
2019_10_02-AM-09_52_28
Theory : reals
Home
Index