Nuprl Definition : compact-dist

dist(x;A) ==  compact-inf{i:l}(d;c;dist-fun(d;x))


Definitions occuring in Statement :  dist-fun: dist-fun(d;x),  compact-inf: compact-inf{i:l}(d;c;f)
Definitions occuring in definition :  dist-fun: dist-fun(d;x),  compact-inf: compact-inf{i:l}(d;c;f)
FDL editor aliases :  compact-dist compact-dist
Latex:
dist(x;A)  ==    compact-inf\{i:l\}(d;c;dist-fun(d;x))


Date html generated: 2019_10_30-AM-07_12_01
Last ObjectModification: 2019_10_25-PM-04_33_20

Theory : reals


Home Index