Nuprl Definition : sphere-map
sphere-map(n) == {f:S(n) ⟶ S(n)| ∀k:ℕ+. ∃d:ℕ+. ∀p,q:S(n). ((d(p;q) ≤ (r1/r(d))) ⇒ (d(f p;f q) ≤ (r1/r(k))))}
Definitions occuring in Statement :
real-unit-sphere: S(n),
real-vec-dist: d(x;y),
rdiv: (x/y),
rleq: x ≤ y,
int-to-real: r(n),
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
exists: ∃x:A. B[x],
nat_plus: ℕ+,
all: ∀x:A. B[x],
real-unit-sphere: S(n),
implies: P ⇒ Q,
rleq: x ≤ y,
real-vec-dist: d(x;y),
add: n + m,
apply: f a,
rdiv: (x/y),
natural_number: $n,
int-to-real: r(n)
FDL editor aliases :
sphere-map
Latex:
sphere-map(n) ==
\{f:S(n) {}\mrightarrow{} S(n)| \mforall{}k:\mBbbN{}\msupplus{}. \mexists{}d:\mBbbN{}\msupplus{}. \mforall{}p,q:S(n). ((d(p;q) \mleq{} (r1/r(d))) {}\mRightarrow{} (d(f p;f q) \mleq{} (r1/r(k))))\}
Date html generated:
2019_10_30-AM-10_15_21
Last ObjectModification:
2019_07_30-PM-02_20_22
Theory : real!vectors
Home
Index