---

Step * of Lemma rv-shift_wf

∀[p:FinProbSpace]. ∀[n:ℕ+]. ∀[X:RandomVariable(p;n)]. ∀[x:Outcome].  (rv-shift(x;X) ∈ RandomVariable(p;n - 1))
BY
{ (Unfolds ``random-variable finite-prob-space p-outcome rv-shift`` 0 THEN Auto) }

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[X:RandomVariable(p;n)].  \mforall{}[x:Outcome].
    (rv-shift(x;X)  \mmember{}  RandomVariable(p;n  -  1))


By

(Unfolds  ``random-variable  finite-prob-space  p-outcome  rv-shift``  0  THEN  Auto)

---

Home Index