---

Step * of Lemma open-random-variable

∀p:FinProbSpace. ∀n:ℕ. ∀C:p-open(p).  (λs.(C <n, s>) ∈ RandomVariable(p;n))
BY
{ ((Unfold `random-variable` 0 THEN Fold `p-outcome` 0) THEN Auto) }

---

Latex:


\mforall{}p:FinProbSpace.  \mforall{}n:\mBbbN{}.  \mforall{}C:p-open(p).    (\mlambda{}s.(C  <n,  s>)  \mmember{}  RandomVariable(p;n))


By

((Unfold  `random-variable`  0  THEN  Fold  `p-outcome`  0)  THEN  Auto)

---

Home Index