Nuprl Definition : metric
metric(X) == {d:X ⟶ X ⟶ ℝ| (∀x,y,z:X. ((d x z) ≤ ((d x y) + (d z y)))) ∧ (∀x:X. ((d x x) = r0))}
Definitions occuring in Statement :
rleq: x ≤ y,
req: x = y,
radd: a + b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
real: ℝ,
and: P ∧ Q,
rleq: x ≤ y,
radd: a + b,
all: ∀x:A. B[x],
req: x = y,
apply: f a,
int-to-real: r(n),
natural_number: $n
FDL editor aliases :
metric
Latex:
metric(X) ==
\{d:X {}\mrightarrow{} X {}\mrightarrow{} \mBbbR{}| (\mforall{}x,y,z:X. ((d x z) \mleq{} ((d x y) + (d z y)))) \mwedge{} (\mforall{}x:X. ((d x x) = r0))\}
Date html generated:
2019_10_29-AM-10_50_33
Last ObjectModification:
2019_10_02-AM-09_32_36
Theory : reals
Home
Index