---

Step * of Lemma rv-disjoint-rv-add2

∀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-add` 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-add`
              THENM  BLemma  `rv-disjoint-symmetry`)
  THEN  Auto)

---

Home Index