Nuprl Definition : vs-lin-indep
vs-lin-indep(K;vs;v.P[v]) ==
∀n:ℕ. ∀f:ℕn + 1 ⟶ {v:Point(vs)| P[v]} .
(Inj(ℕn + 1;Point(vs);f)
⇒ (∀c:ℕn + 1 ⟶ |K|. ((Σ{c i * f i | 0≤i≤n} = 0 ∈ Point(vs)) ⇒ (∀i:ℕn + 1. ((c i) = 0 ∈ |K|)))))
Definitions occuring in Statement :
sum-in-vs: Σ{f[i] | n≤i≤m},
vs-mul: a * x,
vs-0: 0,
vs-point: Point(vs),
inject: Inj(A;B;f),
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n,
equal: s = t ∈ T,
rng_zero: 0,
rng_car: |r|
Definitions occuring in definition :
nat: ℕ,
set: {x:A| B[x]} ,
inject: Inj(A;B;f),
function: x:A ⟶ B[x],
implies: P ⇒ Q,
vs-point: Point(vs),
sum-in-vs: Σ{f[i] | n≤i≤m},
vs-mul: a * x,
vs-0: 0,
all: ∀x:A. B[x],
int_seg: {i..j-},
add: n + m,
natural_number: $n,
equal: s = t ∈ T,
rng_car: |r|,
apply: f a,
rng_zero: 0
FDL editor aliases :
vs-lin-indep
Latex:
vs-lin-indep(K;vs;v.P[v]) ==
\mforall{}n:\mBbbN{}. \mforall{}f:\mBbbN{}n + 1 {}\mrightarrow{} \{v:Point(vs)| P[v]\} .
(Inj(\mBbbN{}n + 1;Point(vs);f)
{}\mRightarrow{} (\mforall{}c:\mBbbN{}n + 1 {}\mrightarrow{} |K|. ((\mSigma{}\{c i * f i | 0\mleq{}i\mleq{}n\} = 0) {}\mRightarrow{} (\mforall{}i:\mBbbN{}n + 1. ((c i) = 0)))))
Date html generated:
2019_10_31-AM-06_26_34
Last ObjectModification:
2019_08_14-PM-06_34_04
Theory : linear!algebra
Home
Index