Nuprl Definition : std-simplex
Δ(n) == {v:ℝ^n + 1| (∀i:ℕn + 1. (r0 ≤ (v i))) ∧ (Σ{v i | 0≤i≤n} = r1)}
Definitions occuring in Statement :
real-vec: ℝ^n,
rsum: Σ{x[k] | n≤k≤m},
rleq: x ≤ y,
req: x = y,
int-to-real: r(n),
int_seg: {i..j-},
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
add: n + m,
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
real-vec: ℝ^n,
and: P ∧ Q,
all: ∀x:A. B[x],
int_seg: {i..j-},
add: n + m,
rleq: x ≤ y,
req: x = y,
rsum: Σ{x[k] | n≤k≤m},
apply: f a,
int-to-real: r(n),
natural_number: $n
FDL editor aliases :
std-simplex
Latex:
\mDelta{}(n) == \{v:\mBbbR{}\^{}n + 1| (\mforall{}i:\mBbbN{}n + 1. (r0 \mleq{} (v i))) \mwedge{} (\mSigma{}\{v i | 0\mleq{}i\mleq{}n\} = r1)\}
Date html generated:
2019_10_30-AM-11_30_23
Last ObjectModification:
2019_07_31-AM-11_29_15
Theory : real!vectors
Home
Index