---

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

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

1
1. p : FinProbSpace
2. a : ℚ
3. f : ℕ ⟶ ℕ
4. X : n:ℕ ⟶ RandomVariable(p;f[n])
5. rv-iid(p;n.f[n];n.X[n])
6. n : ℕ
7. i : ℕn + 1
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:

---

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


By

---

Latex:
xxx(DoSubsume  THEN  Auto  THEN  Auto  THEN  Try  ((Dvar  0  THEN  Complete  (Auto))))xxx

---

Home Index