Nuprl Definition : BrouwerFPT
BrouwerFPT(n) ==
∀f:{f:B(n) ⟶ B(n)| ∀x,y:B(n). (req-vec(n;x;y) ⇒ req-vec(n;f x;f y))} . ∀e:{e:ℝ| r0 < e} . ∃p:B(n). (↓d(f p;p) < e)
Definitions occuring in Statement :
real-unit-ball: B(n),
real-vec-dist: d(x;y),
req-vec: req-vec(n;x;y),
rless: x < y,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
function: x:A ⟶ B[x],
implies: P ⇒ Q,
req-vec: req-vec(n;x;y),
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
real: ℝ,
int-to-real: r(n),
natural_number: $n,
exists: ∃x:A. B[x],
real-unit-ball: B(n),
squash: ↓T,
rless: x < y,
real-vec-dist: d(x;y),
apply: f a
FDL editor aliases :
BrouwerFPT
Latex:
BrouwerFPT(n) ==
\mforall{}f:\{f:B(n) {}\mrightarrow{} B(n)| \mforall{}x,y:B(n). (req-vec(n;x;y) {}\mRightarrow{} req-vec(n;f x;f y))\} . \mforall{}e:\{e:\mBbbR{}| r0 < e\} .
\mexists{}p:B(n). (\mdownarrow{}d(f p;p) < e)
Date html generated:
2019_10_30-AM-11_29_32
Last ObjectModification:
2019_07_30-PM-00_59_10
Theory : real!vectors
Home
Index