Nuprl Definition : metric-eq

metric-eq(X;d;d') ==  ∀x,y:X.  ((d' x y) = (d x y))


Definitions occuring in Statement :  req: x = y,  all: ∀x:A. B[x],  apply: f a
Definitions occuring in definition :  all: ∀x:A. B[x],  req: x = y,  apply: f a
FDL editor aliases :  metric-eq
Latex:
metric-eq(X;d;d')  ==    \mforall{}x,y:X.    ((d'  x  y)  =  (d  x  y))


Date html generated: 2019_10_29-AM-10_51_55
Last ObjectModification: 2019_10_02-AM-09_33_46

Theory : reals


Home Index