---

Step * of Lemma rv-disjoint-symmetry

∀p:FinProbSpace. ∀n:ℕ. ∀X,Y:RandomVariable(p;n).  (rv-disjoint(p;n;X;Y) ⇒ rv-disjoint(p;n;Y;X))
BY
{ (Auto
   THEN RepeatFor 2 (ParallelLast)
   THEN SplitOrHyps
   THEN Try (((OrLeft THENM Trivial)
              THENA (Auto THEN Try ((Fold `random-variable` 0 THEN Auto)) THEN Try ((Fold `p-outcome` 0 THEN Auto)))
              ))
   THEN ((OrRight THENM Trivial)
         THENA (Auto THEN Try ((Fold `random-variable` 0 THEN Auto)) THEN Try ((Fold `p-outcome` 0 THEN Auto)))
         )) }

---

Latex:


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


By

(Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  SplitOrHyps
  THEN  Try  (((OrLeft  THENM  Trivial)
                        THENA  (Auto
                                      THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
                                      THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto)))
                        ))
  THEN  ((OrRight  THENM  Trivial)
              THENA  (Auto
                            THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
                            THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto)))
              ))

---

Home Index