---

Step * of Lemma rv-identically-distributed_wf

∀[p:FinProbSpace]. ∀[f:ℕ ─→ ℕ]. ∀[X:n:ℕ ─→ RandomVariable(p;f[n])].  (rv-identically-distributed(p;n.f[n];n.X[n]) ∈ ℙ)
BY
{ (Unfold `rv-identically-distributed` 0 THEN Auto) }

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])].
    (rv-identically-distributed(p;n.f[n];n.X[n])  \mmember{}  \mBbbP{})


By

(Unfold  `rv-identically-distributed`  0  THEN  Auto)

---

Home Index