---

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


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index