---

Step * 1 of Lemma expectation-rv-disjoint


1. p : FinProbSpace
2. n : ℤ
3. X : RandomVariable(p;0)
4. Y : RandomVariable(p;0)
5. rv-disjoint(p;0;X;Y)
⊢ (X * Y null) = ((X null) * (Y null)) ∈ ℚ
BY
{ ((RepUR ``rv-mul`` 0 THEN Auto) THEN Try ((Fold `random-variable` 0 THEN Auto)) THEN DVar `p' THEN Auto) }

---

Latex:



1.  p  :  FinProbSpace
2.  n  :  \mBbbZ{}
3.  X  :  RandomVariable(p;0)
4.  Y  :  RandomVariable(p;0)
5.  rv-disjoint(p;0;X;Y)
\mvdash{}  (X  *  Y  null)  =  ((X  null)  *  (Y  null))


By

((RepUR  ``rv-mul``  0  THEN  Auto)
  THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
  THEN  DVar  `p'
  THEN  Auto)

---

Home Index