Nuprl Definition : unit-ball-approx
unit-ball-approx(n;k) == {x:ℕn ⟶ {-k..k + 1-}| Σ((x i) * (x i) | i < n) ≤ (k * k)}
Definitions occuring in Statement :
sum: Σ(f[x] | x < k),
int_seg: {i..j-},
le: A ≤ B,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
multiply: n * m,
add: n + m,
minus: -n,
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
int_seg: {i..j-},
minus: -n,
add: n + m,
natural_number: $n,
le: A ≤ B,
sum: Σ(f[x] | x < k),
apply: f a,
multiply: n * m
FDL editor aliases :
unit-ball-approx
Latex:
unit-ball-approx(n;k) == \{x:\mBbbN{}n {}\mrightarrow{} \{-k..k + 1\msupminus{}\}| \mSigma{}((x i) * (x i) | i < n) \mleq{} (k * k)\}
Date html generated:
2019_10_30-AM-11_27_58
Last ObjectModification:
2019_06_28-PM-01_56_03
Theory : real!vectors
Home
Index