---

Step * of Lemma random-variable_wf

∀[k:FinProbSpace]. ∀[n:ℕ].  (RandomVariable(k;n) ∈ Type)
BY
{ (Unfolds ``finite-prob-space random-variable`` 0 THEN Auto) }

---

Latex:


\mforall{}[k:FinProbSpace].  \mforall{}[n:\mBbbN{}].    (RandomVariable(k;n)  \mmember{}  Type)


By

(Unfolds  ``finite-prob-space  random-variable``  0  THEN  Auto)

---

Home Index