Nuprl Definition : vector-space
VectorSpace(K) ==
"Point":Type
"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) ∈ Point(self)))
∧ (∀x,y:Point(self). ((f x y) = (f y x) ∈ Point(self)))}
"*":{m:|K| ⟶ Point(self) ⟶ Point(self)|
(∀a:|K|. ∀x,y:Point(self). ((m a (self."+" x y)) = (self."+" (m a x) (m a y)) ∈ Point(self)))
∧ (∀x:Point(self)
(((m 1 x) = x ∈ Point(self))
∧ ((m 0 x) = self."0" ∈ Point(self))
∧ (∀a,b:|K|. ((m a (m b x)) = (m (a * b) x) ∈ Point(self)))
∧ (∀a,b:|K|. ((m (a +K b) x) = (self."+" (m a x) (m b x)) ∈ Point(self)))))}
Definitions occuring in Statement :
vs-point: Point(vs),
top: Top,
infix_ap: x f y,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
token: "$token",
universe: Type,
equal: s = t ∈ T,
rng_one: 1,
rng_times: *,
rng_zero: 0,
rng_plus: +r,
rng_car: |r|,
record-select: r.x,
record+: record+,
record: record(x.T[x])
Definitions occuring in definition :
apply: f a,
vs-point: Point(vs),
equal: s = t ∈ T,
rng_car: |r|,
all: ∀x:A. B[x],
and: P ∧ Q,
token: "$token",
record-select: r.x,
rng_zero: 0,
rng_one: 1,
function: x:A ⟶ B[x],
set: {x:A| B[x]} ,
universe: Type,
top: Top,
record: record(x.T[x]),
record+: record+,
infix_ap: x f y,
rng_times: *,
rng_plus: +r
FDL editor aliases :
vsp
Latex:
VectorSpace(K) ==
"Point":Type
"0":Point(self)
"+":\{f:Point(self) {}\mrightarrow{} Point(self) {}\mrightarrow{} Point(self)|
(\mforall{}x,y,z:Point(self). ((f x (f y z)) = (f (f x y) z)))
\mwedge{} (\mforall{}x,y:Point(self). ((f x y) = (f y x)))\}
"*":\{m:|K| {}\mrightarrow{} Point(self) {}\mrightarrow{} Point(self)|
(\mforall{}a:|K|. \mforall{}x,y:Point(self). ((m a (self."+" x y)) = (self."+" (m a x) (m a y))))
\mwedge{} (\mforall{}x:Point(self)
(((m 1 x) = x)
\mwedge{} ((m 0 x) = self."0")
\mwedge{} (\mforall{}a,b:|K|. ((m a (m b x)) = (m (a * b) x)))
\mwedge{} (\mforall{}a,b:|K|. ((m (a +K b) x) = (self."+" (m a x) (m b x))))))\}
Date html generated:
2018_05_22-PM-09_40_09
Last ObjectModification:
2017_11_02-PM-03_21_55
Theory : linear!algebra
Home
Index