---

Step * 1 1 1 of Lemma open-expectation-monotone


1. p : FinProbSpace
2. n : ℤ
3. m : ℕ@i
4. 0 ≤ m@i
5. C : p-open(p)@i
⊢ λs.(C <0, null>) ≤ λs.(C <m, s>)
BY
{ (RepUR ``rv-le`` 0 THEN Auto) }

1
1. p : FinProbSpace
2. n : ℤ
3. m : ℕ@i
4. 0 ≤ m@i
5. C : p-open(p)@i
6. s : ℕm ─→ Outcome@i
⊢ (C <0, null>) ≤ (C <m, s>)

---

Latex:



1.  p  :  FinProbSpace
2.  n  :  \mBbbZ{}
3.  m  :  \mBbbN{}@i
4.  0  \mleq{}  m@i
5.  C  :  p-open(p)@i
\mvdash{}  \mlambda{}s.(C  ɘ,  null>)  \mleq{}  \mlambda{}s.(C  <m,  s>)


By

(RepUR  ``rv-le``  0  THEN  Auto)

---

Home Index