---

Step * of Lemma rv-sample_wf

∀[k:FinProbSpace]. ∀[n:ℕ]. ∀[i:ℕn]. ∀[X:Outcome ─→ ℚ].  (X@i ∈ RandomVariable(k;n))
BY
{ (Unfolds ``finite-prob-space p-outcome rv-sample random-variable`` 0 THEN Auto) }

---

Latex:


\mforall{}[k:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[i:\mBbbN{}n].  \mforall{}[X:Outcome  {}\mrightarrow{}  \mBbbQ{}].    (X@i  \mmember{}  RandomVariable(k;n))


By

(Unfolds  ``finite-prob-space  p-outcome  rv-sample  random-variable``  0  THEN  Auto)

---

Home Index