Nuprl Definition : finite-prob-space
FinProbSpace == {p:ℚ List| (Σ0 ≤ i < ||p||. p[i] = 1 ∈ ℚ) ∧ (∀q∈p.0 ≤ q)}
Definitions occuring in Statement :
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,
rationals: ℚ
FDL editor aliases :
finite-prob-space
FinProbSpace == \{p:\mBbbQ{} List| (\mSigma{}0 \mleq{} i < ||p||. p[i] = 1) \mwedge{} (\mforall{}q\mmember{}p.0 \mleq{} q)\}
Date html generated:
2015_07_17-AM-07_57_54
Last ObjectModification:
2012_06_27-AM-02_11_40
Home
Index