Nuprl Definition : real-vector-space
RealVectorSpace ==
SeparationSpace
"0":Point(self)
"+":{f:Point(self) ⟶ Point(self) ⟶ Point(self)|
(∀x,y,z:Point(self). f x (f y z) ≡ f (f x y) z) ∧ (∀x,y:Point(self). f x y ≡ f y x)}
"+sep":∀x,x',y,y':Point(self). (self."+" x y # self."+" x' y' ⇒ (x # x' ∨ y # y'))
"*":{m:ℝ ⟶ Point(self) ⟶ Point(self)|
(∀a:ℝ. ∀x,y:Point(self). m a (self."+" x y) ≡ self."+" (m a x) (m a y))
∧ (∀x:Point(self)
(m r1 x ≡ x
∧ m r0 x ≡ self."0"
∧ (∀a,b:ℝ. m a (m b x) ≡ m (a * b) x)
∧ (∀a,b:ℝ. m (a + b) x ≡ self."+" (m a x) (m b x))))}
"*sep":∀a,b:ℝ. ∀x,y:Point(self). (self."*" a x # self."*" b y ⇒ (a ≠ b ∨ x # y))
Definitions occuring in Statement :
ss-eq: x ≡ y,
ss-sep: x # y,
ss-point: Point(ss),
separation-space: SeparationSpace,
rneq: x ≠ y,
rmul: a * b,
radd: a + b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
token: "$token",
record-select: r.x,
record+: record+
Definitions occuring in definition :
apply: f a,
radd: a + b,
real: ℝ,
all: ∀x:A. B[x],
rmul: a * b,
and: P ∧ Q,
token: "$token",
record-select: r.x,
natural_number: $n,
int-to-real: r(n),
function: x:A ⟶ B[x],
set: {x:A| B[x]} ,
or: P ∨ Q,
implies: P ⇒ Q,
record+: record+,
rneq: x ≠ y
FDL editor aliases :
rv-sp
Latex:
RealVectorSpace ==
SeparationSpace
"0":Point(self)
"+":\{f:Point(self) {}\mrightarrow{} Point(self) {}\mrightarrow{} Point(self)|
(\mforall{}x,y,z:Point(self). f x (f y z) \mequiv{} f (f x y) z) \mwedge{} (\mforall{}x,y:Point(self). f x y \mequiv{} f y x)\}
"+sep":\mforall{}x,x',y,y':Point(self). (self."+" x y \# self."+" x' y' {}\mRightarrow{} (x \# x' \mvee{} y \# y'))
"*":\{m:\mBbbR{} {}\mrightarrow{} Point(self) {}\mrightarrow{} Point(self)|
(\mforall{}a:\mBbbR{}. \mforall{}x,y:Point(self). m a (self."+" x y) \mequiv{} self."+" (m a x) (m a y))
\mwedge{} (\mforall{}x:Point(self)
(m r1 x \mequiv{} x
\mwedge{} m r0 x \mequiv{} self."0"
\mwedge{} (\mforall{}a,b:\mBbbR{}. m a (m b x) \mequiv{} m (a * b) x)
\mwedge{} (\mforall{}a,b:\mBbbR{}. m (a + b) x \mequiv{} self."+" (m a x) (m b x))))\}
"*sep":\mforall{}a,b:\mBbbR{}. \mforall{}x,y:Point(self). (self."*" a x \# self."*" b y {}\mRightarrow{} (a \mneq{} b \mvee{} x \# y))
Date html generated:
2019_10_31-AM-07_27_59
Last ObjectModification:
2017_06_22-PM-06_44_07
Theory : inner!product!spaces
Home
Index