---

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


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index