Nuprl Definition : IdNotHomotopicConst
IdNotHomotopicConst(n) ==
¬(∃h:{t:ℝ| t ∈ [r0, r1]} ⟶ S(n) ⟶ S(n)
((∀p:S(n). req-vec(n + 1;h r1 p;p))
∧ (∃q:S(n). ∀p:S(n). req-vec(n + 1;h r0 p;q))
∧ (∀t1,t2:{t:ℝ| t ∈ [r0, r1]} . ∀p1,p2:S(n).
((t1 = t2) ⇒ req-vec(n + 1;p1;p2) ⇒ req-vec(n + 1;h t1 p1;h t2 p2)))))
Definitions occuring in Statement :
real-unit-sphere: S(n),
req-vec: req-vec(n;x;y),
rccint: [l, u],
i-member: r ∈ I,
req: x = y,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: 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 :
not: ¬A,
function: x:A ⟶ B[x],
and: P ∧ Q,
exists: ∃x:A. B[x],
set: {x:A| B[x]} ,
real: ℝ,
i-member: r ∈ I,
rccint: [l, u],
int-to-real: r(n),
all: ∀x:A. B[x],
real-unit-sphere: S(n),
req: x = y,
implies: P ⇒ Q,
req-vec: req-vec(n;x;y),
add: n + m,
natural_number: $n,
apply: f a
FDL editor aliases :
IdNotHomotopicConst
Latex:
IdNotHomotopicConst(n) ==
\mneg{}(\mexists{}h:\{t:\mBbbR{}| t \mmember{} [r0, r1]\} {}\mrightarrow{} S(n) {}\mrightarrow{} S(n)
((\mforall{}p:S(n). req-vec(n + 1;h r1 p;p))
\mwedge{} (\mexists{}q:S(n). \mforall{}p:S(n). req-vec(n + 1;h r0 p;q))
\mwedge{} (\mforall{}t1,t2:\{t:\mBbbR{}| t \mmember{} [r0, r1]\} . \mforall{}p1,p2:S(n).
((t1 = t2) {}\mRightarrow{} req-vec(n + 1;p1;p2) {}\mRightarrow{} req-vec(n + 1;h t1 p1;h t2 p2)))))
Date html generated:
2019_10_30-AM-11_29_54
Last ObjectModification:
2019_08_05-PM-03_54_07
Theory : real!vectors
Home
Index