Nuprl Definition : ss-homotopic
ss-homotopic(X;x0;x1;a;b) ==
∃p:Point(Path(Path(X))). (p@r0 ≡ a ∧ p@r1 ≡ b ∧ (∀t:{t:ℝ| t ∈ [r0, r1]} . (p@t@r0 ≡ x0 ∧ p@t@r1 ≡ x1)))
Definitions occuring in Statement :
path-at: p@t,
path-ss: Path(X),
ss-eq: x ≡ y,
ss-point: Point(ss),
rccint: [l, u],
i-member: r ∈ I,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions occuring in definition :
exists: ∃x:A. B[x],
ss-point: Point(ss),
path-ss: Path(X),
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
real: ℝ,
i-member: r ∈ I,
rccint: [l, u],
and: P ∧ Q,
ss-eq: x ≡ y,
path-at: p@t,
int-to-real: r(n),
natural_number: $n
FDL editor aliases :
ss-homotopic
Latex:
ss-homotopic(X;x0;x1;a;b) ==
\mexists{}p:Point(Path(Path(X)))
(p@r0 \mequiv{} a \mwedge{} p@r1 \mequiv{} b \mwedge{} (\mforall{}t:\{t:\mBbbR{}| t \mmember{} [r0, r1]\} . (p@t@r0 \mequiv{} x0 \mwedge{} p@t@r1 \mequiv{} x1)))
Date html generated:
2020_05_20-PM-01_20_31
Last ObjectModification:
2018_07_05-PM-03_50_49
Theory : intuitionistic!topology
Home
Index