---

Step * of Lemma rv-scale_wf

∀[k:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(k;n)]. ∀[q:ℚ].  (q*X ∈ RandomVariable(k;n))
BY
{ (Unfolds ``random-variable finite-prob-space rv-scale`` 0 THEN Auto)⋅ }

---

Latex:


\mforall{}[k:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X:RandomVariable(k;n)].  \mforall{}[q:\mBbbQ{}].    (q*X  \mmember{}  RandomVariable(k;n))


By

(Unfolds  ``random-variable  finite-prob-space  rv-scale``  0  THEN  Auto)\mcdot{}

---

Home Index