---

Step * of Lemma rv-disjoint-const

∀p:FinProbSpace. ∀n:ℕ. ∀X:RandomVariable(p;n). ∀a:ℚ.  rv-disjoint(p;n;a;X)
BY
{ Auto }

1
1. p : FinProbSpace@i
2. n : ℕ@i
3. X : RandomVariable(p;n)@i
4. a : ℚ@i
⊢ rv-disjoint(p;n;a;X)

---

Latex:


\mforall{}p:FinProbSpace.  \mforall{}n:\mBbbN{}.  \mforall{}X:RandomVariable(p;n).  \mforall{}a:\mBbbQ{}.    rv-disjoint(p;n;a;X)


By

Auto

---

Home Index