Nuprl Definition : DegreeExists
DegreeExists(n) ==
∃ind:sphere-map(n) ⟶ ℤ
((∀f,g:sphere-map(n). (sphere-map-eq(n;f;g) ⇒ ((ind f) = (ind g) ∈ ℤ)))
∧ (∀p:S(n). ((ind const-sphere-map(p)) = 0 ∈ ℤ))
∧ ((ind id-sphere-map()) = 1 ∈ ℤ))
Definitions occuring in Statement :
id-sphere-map: id-sphere-map(),
const-sphere-map: const-sphere-map(p),
sphere-map-eq: sphere-map-eq(n;f;g),
sphere-map: sphere-map(n),
real-unit-sphere: S(n),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
sphere-map: sphere-map(n),
implies: P ⇒ Q,
sphere-map-eq: sphere-map-eq(n;f;g),
and: P ∧ Q,
all: ∀x:A. B[x],
real-unit-sphere: S(n),
const-sphere-map: const-sphere-map(p),
equal: s = t ∈ T,
int: ℤ,
apply: f a,
id-sphere-map: id-sphere-map(),
natural_number: $n
FDL editor aliases :
DegreeExists
Latex:
DegreeExists(n) ==
\mexists{}ind:sphere-map(n) {}\mrightarrow{} \mBbbZ{}
((\mforall{}f,g:sphere-map(n). (sphere-map-eq(n;f;g) {}\mRightarrow{} ((ind f) = (ind g))))
\mwedge{} (\mforall{}p:S(n). ((ind const-sphere-map(p)) = 0))
\mwedge{} ((ind id-sphere-map()) = 1))
Date html generated:
2019_10_30-AM-11_30_08
Last ObjectModification:
2019_08_06-AM-11_40_19
Theory : real!vectors
Home
Index