Step * of Lemma rv-mul_wf

[k:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(k;n)].  (X Y ∈ RandomVariable(k;n))
BY
(Unfolds ``random-variable finite-prob-space rv-mul`` THEN Auto) }


Latex:


Latex:
\mforall{}[k:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X,Y:RandomVariable(k;n)].    (X  *  Y  \mmember{}  RandomVariable(k;n))


By


Latex:
(Unfolds  ``random-variable  finite-prob-space  rv-mul``  0  THEN  Auto)




Home Index