---

Step * of Lemma open-expectation-monotone

∀[p:FinProbSpace]. ∀[n,m:ℕ].  ∀[C:p-open(p)]. (E(n;λs.(C <n, s>)) ≤ E(m;λs.(C <m, s>))) supposing n ≤ m
BY
{ xxx(Auto
      THEN Try ((BLemma `open-random-variable`  THEN Auto))
      THEN RepeatFor 3 (MoveToConcl (-1))
      THEN NatInd (-1)
      THEN Auto)xxx }

1
1. p : FinProbSpace
2. n : ℤ
3. m : ℕ
4. 0 ≤ m
5. C : p-open(p)
⊢ E(0;λs.(C <0, s>)) ≤ E(m;λs.(C <m, s>))

2
1. p : FinProbSpace
2. n : ℤ
3. 0 < n
4. ∀m:ℕ. (((n - 1) ≤ m) ⇒ (∀C:p-open(p). (E(n - 1;λs.(C <n - 1, s>)) ≤ E(m;λs.(C <m, s>)))))
5. m : ℕ
6. n ≤ m
7. C : p-open(p)
⊢ E(n;λs.(C <n, s>)) ≤ E(m;λs.(C <m, s>))

---

Latex:

---

Latex:
\mforall{}[p:FinProbSpace].  \mforall{}[n,m:\mBbbN{}].    \mforall{}[C:p-open(p)].  (E(n;\mlambda{}s.(C  <n,  s>))  \mleq{}  E(m;\mlambda{}s.(C  <m,  s>)))  supposing  n  \000C\mleq{}  m


By

---

Latex:
xxx(Auto
        THEN  Try  ((BLemma  `open-random-variable`    THEN  Auto))
        THEN  RepeatFor  3  (MoveToConcl  (-1))
        THEN  NatInd  (-1)
        THEN  Auto)xxx

---

Home Index