Nuprl Definition : finite-prob-space
FinProbSpace == {p:ℚ List| (Σ0 ≤ i < ||p||. p[i] = 1 ∈ ℚ) ∧ (∀q∈p.0 ≤ q)}
Definitions occuring in Statement :
qsum: Σa ≤ j < b. E[j],
qle: r ≤ s,
rationals: ℚ,
l_all: (∀x∈L.P[x]),
select: L[n],
length: ||as||,
list: T List,
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n,
equal: s = t ∈ T
FDL editor aliases :
finite-prob-space
Latex:
FinProbSpace == \{p:\mBbbQ{} List| (\mSigma{}0 \mleq{} i < ||p||. p[i] = 1) \mwedge{} (\mforall{}q\mmember{}p.0 \mleq{} q)\}
Date html generated:
2016_05_15-PM-11_44_38
Last ObjectModification:
2012_06_27-AM-02_11_40
Theory : randomness
Home
Index