---

Step * 1 1 1 of Lemma expectation-monotone-in-first


1. p : FinProbSpace
2. n : ℤ
3. m : ℕ
4. 0 ≤ m
5. X : RandomVariable(p;0)
6. s : ℕm ─→ Outcome@i
⊢ (X s) = (X null) ∈ ℚ
BY
{ (Unfold `random-variable` -2 THEN (EqCD THEN Auto) THEN Ext THEN Auto) }

---

Latex:



1.  p  :  FinProbSpace
2.  n  :  \mBbbZ{}
3.  m  :  \mBbbN{}
4.  0  \mleq{}  m
5.  X  :  RandomVariable(p;0)
6.  s  :  \mBbbN{}m  {}\mrightarrow{}  Outcome@i
\mvdash{}  (X  s)  =  (X  null)


By

(Unfold  `random-variable`  -2  THEN  (EqCD  THEN  Auto)  THEN  Ext  THEN  Auto)

---

Home Index