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: List and: P ∧ Q set: {x:A| B[x]}  natural_number: $n equal: 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