Nuprl Definition : NoBallRetraction
NoBallRetraction(n) ==
¬(∃g:B(n) ⟶ B(n)
((∀x,y:B(n). (req-vec(n;x;y) ⇒ req-vec(n;g x;g y)))
∧ (∀x:B(n). (||g x|| = r1))
∧ (∀x:B(n). ((||x|| = r1) ⇒ req-vec(n;g x;x)))))
Definitions occuring in Statement :
real-unit-ball: B(n),
real-vec-norm: ||x||,
req-vec: req-vec(n;x;y),
req: x = y,
int-to-real: r(n),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
not: ¬A,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
and: P ∧ Q,
all: ∀x:A. B[x],
real-unit-ball: B(n),
implies: P ⇒ Q,
req: x = y,
real-vec-norm: ||x||,
int-to-real: r(n),
natural_number: $n,
req-vec: req-vec(n;x;y),
apply: f a
FDL editor aliases :
NoBallRetraction
Latex:
NoBallRetraction(n) ==
\mneg{}(\mexists{}g:B(n) {}\mrightarrow{} B(n)
((\mforall{}x,y:B(n). (req-vec(n;x;y) {}\mRightarrow{} req-vec(n;g x;g y)))
\mwedge{} (\mforall{}x:B(n). (||g x|| = r1))
\mwedge{} (\mforall{}x:B(n). ((||x|| = r1) {}\mRightarrow{} req-vec(n;g x;x)))))
Date html generated:
2019_10_30-AM-11_29_38
Last ObjectModification:
2019_07_08-PM-09_27_47
Theory : real!vectors
Home
Index