---

Step * of Lemma rv-disjoint_wf

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].  (rv-disjoint(p;n;X;Y) ∈ ℙ)
BY
{ (Unfolds ``rv-disjoint random-variable`` 0 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)  \mmember{}  \mBbbP{})


By

(Unfolds  ``rv-disjoint  random-variable``  0  THEN  Try  (Fold  `p-outcome`  0)  THEN  Auto)

---

Home Index