---

Step * of Lemma rv-unbounded_wf

∀[p:FinProbSpace]. ∀[f:ℕ ─→ ℕ]. ∀[X:n:ℕ ─→ RandomVariable(p;f[n])].  ((X[n]─→∞ as n─→∞) ∈ (ℕ ─→ Outcome) ─→ ℙ)
BY
{ (Auto
   THEN Unfold `rv-unbounded` 0
   THEN Auto
   THEN Try ((Fold `p-outcome` 0 THEN Auto))
   THEN Try (Unfold `p-outcome` 0)
   THEN Try (Fold `random-variable` 0)
   THEN Auto) }

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])].
    ((X[n]{}\mrightarrow{}\minfty{}  as  n{}\mrightarrow{}\minfty{})  \mmember{}  (\mBbbN{}  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbP{})


By

(Auto
  THEN  Unfold  `rv-unbounded`  0
  THEN  Auto
  THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto))
  THEN  Try  (Unfold  `p-outcome`  0)
  THEN  Try  (Fold  `random-variable`  0)
  THEN  Auto)

---

Home Index