Nuprl Definition : real-vec-indep
real-vec-indep(k;L) == ∀a:ℕ||L|| ⟶ ℝ. (req-vec(k;Σ{a i*L[i] | 0≤i≤||L|| - 1};λi.r0) ⇒ (∀i:ℕ||L||. ((a i) = r0)))
Definitions occuring in Statement :
real-vec-sum: Σ{x[k] | n≤k≤m},
real-vec-mul: a*X,
req-vec: req-vec(n;x;y),
req: x = y,
int-to-real: r(n),
real: ℝ,
select: L[n],
length: ||as||,
int_seg: {i..j-},
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
function: x:A ⟶ B[x],
real: ℝ,
implies: P ⇒ Q,
req-vec: req-vec(n;x;y),
real-vec-sum: Σ{x[k] | n≤k≤m},
subtract: n - m,
real-vec-mul: a*X,
select: L[n],
lambda: λx.A[x],
all: ∀x:A. B[x],
int_seg: {i..j-},
length: ||as||,
req: x = y,
apply: f a,
int-to-real: r(n),
natural_number: $n
FDL editor aliases :
real-vec-indep
Latex:
real-vec-indep(k;L) ==
\mforall{}a:\mBbbN{}||L|| {}\mrightarrow{} \mBbbR{}. (req-vec(k;\mSigma{}\{a i*L[i] | 0\mleq{}i\mleq{}||L|| - 1\};\mlambda{}i.r0) {}\mRightarrow{} (\mforall{}i:\mBbbN{}||L||. ((a i) = r0)))
Date html generated:
2019_10_30-AM-08_03_37
Last ObjectModification:
2019_09_17-PM-05_50_23
Theory : reals
Home
Index