Nuprl Definition : sphere-map-eq
sphere-map-eq(n;f;g) == ∀p:S(n). req-vec(n + 1;f p;g p)
Definitions occuring in Statement :
real-unit-sphere: S(n)
,
req-vec: req-vec(n;x;y)
,
all: ∀x:A. B[x]
,
apply: f a
,
add: n + m
,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x]
,
real-unit-sphere: S(n)
,
req-vec: req-vec(n;x;y)
,
add: n + m
,
natural_number: $n
,
apply: f a
FDL editor aliases :
sphere-map-eq
Latex:
sphere-map-eq(n;f;g) == \mforall{}p:S(n). req-vec(n + 1;f p;g p)
Date html generated:
2019_10_30-AM-10_15_25
Last ObjectModification:
2019_07_30-AM-09_27_17
Theory : real!vectors
Home
Index