---

Step * of Lemma rv-disjoint-rv-mul2

∀p:FinProbSpace. ∀n:ℕ. ∀X,Y,Z:RandomVariable(p;n).
  (rv-disjoint(p;n;Y;X) ⇒ rv-disjoint(p;n;Z;X) ⇒ rv-disjoint(p;n;Y * Z;X))
BY
{ (Auto
   THEN (BLemma `rv-disjoint-symmetry` THENM BLemma `rv-disjoint-rv-mul` THENM BLemma `rv-disjoint-symmetry`)
   THEN Auto) }

---

Latex:


\mforall{}p:FinProbSpace.  \mforall{}n:\mBbbN{}.  \mforall{}X,Y,Z:RandomVariable(p;n).
    (rv-disjoint(p;n;Y;X)  {}\mRightarrow{}  rv-disjoint(p;n;Z;X)  {}\mRightarrow{}  rv-disjoint(p;n;Y  *  Z;X))


By

(Auto
  THEN  (BLemma  `rv-disjoint-symmetry`
              THENM  BLemma  `rv-disjoint-rv-mul`
              THENM  BLemma  `rv-disjoint-symmetry`)
  THEN  Auto)

---

Home Index