---

Step * 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])
⊢ rv-iid(p;n.f[n];n.a)
BY
{ xxx(RepeatFor 2 (ParallelLast) THEN Auto THEN Try ((BLemma `rv-disjoint-const` THEN Auto)))xxx }

1
1. p : FinProbSpace
2. a : ℚ
3. f : ℕ ⟶ ℕ
4. X : n:ℕ ⟶ RandomVariable(p;f[n])
5. ∀n:ℕ. ∀n@0:ℕn.  (f[n@0] < f[n] ∧ rv-disjoint(p;f[n];X[n@0];X[n]))
6. rv-identically-distributed(p;n.f[n];n.X[n])
⊢ rv-identically-distributed(p;n.f[n];n.a)

---

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])
\mvdash{}  rv-iid(p;n.f[n];n.a)


By

---

Latex:
xxx(RepeatFor  2  (ParallelLast)  THEN  Auto  THEN  Try  ((BLemma  `rv-disjoint-const`  THEN  Auto)))xxx

---

Home Index