Nuprl Definition : real-vec-free
real-vec-free(k;L) == ∀a:ℕ||L|| ⟶ ℝ. (a ≠ λi.r0 ⇒ Σ{a i*L[i] | 0≤i≤||L|| - 1} ≠ λi.r0)
Definitions occuring in Statement :
real-vec-sep: a ≠ b,
real-vec-sum: Σ{x[k] | n≤k≤m},
real-vec-mul: a*X,
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 :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
int_seg: {i..j-},
real: ℝ,
implies: P ⇒ Q,
real-vec-sum: Σ{x[k] | n≤k≤m},
subtract: n - m,
length: ||as||,
real-vec-mul: a*X,
apply: f a,
select: L[n],
lambda: λx.A[x],
int-to-real: r(n),
natural_number: $n
FDL editor aliases :
real-vec-free
Latex:
real-vec-free(k;L) == \mforall{}a:\mBbbN{}||L|| {}\mrightarrow{} \mBbbR{}. (a \mneq{} \mlambda{}i.r0 {}\mRightarrow{} \mSigma{}\{a i*L[i] | 0\mleq{}i\mleq{}||L|| - 1\} \mneq{} \mlambda{}i.r0)
Date html generated:
2019_10_30-AM-08_44_41
Last ObjectModification:
2019_09_18-PM-01_49_37
Theory : reals
Home
Index