---

Step * 2 of Lemma rv-iid-add-const

.....wf..... 
1. p : FinProbSpace@i
2. a : ℚ@i
3. f : ℕ ─→ ℕ@i
4. X : n:ℕ ─→ RandomVariable(p;f[n])@i
5. rv-iid(p;n.f[n];n.X[n])@i
6. n : ℕ@i
7. i : ℕn + 1@i
8. rv-disjoint(p;f[n];a;X[n])
⊢ X[i] ∈ RandomVariable(p;f[n])
BY
{ (DoSubsume THEN Auto THEN Auto THEN Try ((Dvar 0 THEN Complete (Auto)))) }

1
1. p : FinProbSpace@i
2. a : ℚ@i
3. f : ℕ ─→ ℕ@i
4. X : n:ℕ ─→ RandomVariable(p;f[n])@i
5. rv-iid(p;n.f[n];n.X[n])@i
6. n : ℕ@i
7. i : ℕn + 1@i
8. rv-disjoint(p;f[n];a;X[n])
9. X[i] = X[i] ∈ RandomVariable(p;f[i])
⊢ RandomVariable(p;f[i]) ⊆r RandomVariable(p;f[n])

---

Latex:


.....wf..... 
1.  p  :  FinProbSpace@i
2.  a  :  \mBbbQ{}@i
3.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
4.  X  :  n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])@i
5.  rv-iid(p;n.f[n];n.X[n])@i
6.  n  :  \mBbbN{}@i
7.  i  :  \mBbbN{}n  +  1@i
8.  rv-disjoint(p;f[n];a;X[n])
\mvdash{}  X[i]  \mmember{}  RandomVariable(p;f[n])


By

(DoSubsume  THEN  Auto  THEN  Auto  THEN  Try  ((Dvar  0  THEN  Complete  (Auto))))

---

Home Index