Nuprl Definition : vs-subspace
vs-subspace(K;vs;x.P[x]) ==
P[0] ∧ (∀x,y:Point(vs). (P[x] ⇒ P[y] ⇒ P[x + y])) ∧ (∀x:Point(vs). ∀a:|K|. (P[x] ⇒ P[a * x]))
Definitions occuring in Statement :
vs-mul: a * x,
vs-add: x + y,
vs-0: 0,
vs-point: Point(vs),
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
rng_car: |r|
Definitions occuring in definition :
vs-0: 0,
and: P ∧ Q,
vs-add: x + y,
vs-point: Point(vs),
all: ∀x:A. B[x],
rng_car: |r|,
implies: P ⇒ Q,
vs-mul: a * x
FDL editor aliases :
vs-subspace
Latex:
vs-subspace(K;vs;x.P[x]) ==
P[0] \mwedge{} (\mforall{}x,y:Point(vs). (P[x] {}\mRightarrow{} P[y] {}\mRightarrow{} P[x + y])) \mwedge{} (\mforall{}x:Point(vs). \mforall{}a:|K|. (P[x] {}\mRightarrow{} P[a * x]))
Date html generated:
2018_05_22-PM-09_41_57
Last ObjectModification:
2017_11_03-PM-00_23_34
Theory : linear!algebra
Home
Index