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