---

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
{ xxx(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)))
            ))xxx }

---

Latex:

---

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

---

Latex:
xxx(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)))
                    ))xxx

---

Home Index