Nuprl Definition : vs-map
A ⟶ B ==
{f:Point(A) ⟶ Point(B)|
(∀u,v:Point(A). ((f u + v) = f u + f v ∈ Point(B))) ∧ (∀a:|K|. ∀u:Point(A). ((f a * u) = a * f u ∈ Point(B)))}
Definitions occuring in Statement :
vs-mul: a * x,
vs-add: x + y,
vs-point: Point(vs),
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T,
rng_car: |r|
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
and: P ∧ Q,
vs-add: x + y,
rng_car: |r|,
all: ∀x:A. B[x],
equal: s = t ∈ T,
vs-point: Point(vs),
vs-mul: a * x,
apply: f a
FDL editor aliases :
vs-map
Latex:
A {}\mrightarrow{} B ==
\{f:Point(A) {}\mrightarrow{} Point(B)|
(\mforall{}u,v:Point(A). ((f u + v) = f u + f v)) \mwedge{} (\mforall{}a:|K|. \mforall{}u:Point(A). ((f a * u) = a * f u))\}
Date html generated:
2018_05_22-PM-09_42_44
Last ObjectModification:
2017_11_02-PM-05_20_40
Theory : linear!algebra
Home
Index