---

Step * of Lemma rv-compose_wf

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)]. ∀[F:ℚ ─→ ℚ].  ((X.F[X]) o X ∈ RandomVariable(p;n))
BY
{ (Unfolds ``random-variable rv-compose`` 0 THEN Try (Fold`p-outcome` 0) THEN Auto) }

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X:RandomVariable(p;n)].  \mforall{}[F:\mBbbQ{}  {}\mrightarrow{}  \mBbbQ{}].
    ((X.F[X])  o  X  \mmember{}  RandomVariable(p;n))


By

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

---

Home Index