---

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

.....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]
BY
{ (Decide ⌈i = n ∈ ℤ⌉⋅ THEN Auto) }

---

Latex:


.....assertion..... 
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{}  f[i]  \mleq{}  f[n]


By

(Decide  \mkleeneopen{}i  =  n\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index