---

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


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])
BY
{ (Assert ⌈f[i] ≤ f[n]⌉⋅ THEN Auto) }

1
.....assertion..... 
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])
⊢ f[i] ≤ f[n]

---

Latex:



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])
9.  X[i]  =  X[i]
\mvdash{}  RandomVariable(p;f[i])  \msubseteq{}r  RandomVariable(p;f[n])


By

(Assert  \mkleeneopen{}f[i]  \mleq{}  f[n]\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index