---

Step * of Lemma rv-const_wf

∀[p:FinProbSpace]. ∀[a:ℚ]. ∀[n:ℕ].  (a ∈ RandomVariable(p;n))
BY
{ (Unfolds ``finite-prob-space rv-const random-variable`` 0 THEN Auto) }

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[a:\mBbbQ{}].  \mforall{}[n:\mBbbN{}].    (a  \mmember{}  RandomVariable(p;n))


By

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

---

Home Index