---

Step * of Lemma expectation_wf

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)].  (E(n;X) ∈ ℚ)
BY
{ xxx(Unfold `finite-prob-space` 0
      THEN InductionOnNat
      THEN RecUnfold `expectation` 0
      THEN Reduce 0
      THEN Try ((SplitOnConclITE THENA Auto))
      THEN Auto
      THEN Try ((Fold `random-variable` 0 THEN Auto)))xxx }

---

Latex:

---

Latex:
\mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X:RandomVariable(p;n)].    (E(n;X)  \mmember{}  \mBbbQ{})


By

---

Latex:
xxx(Unfold  `finite-prob-space`  0
        THEN  InductionOnNat
        THEN  RecUnfold  `expectation`  0
        THEN  Reduce  0
        THEN  Try  ((SplitOnConclITE  THENA  Auto))
        THEN  Auto
        THEN  Try  ((Fold  `random-variable`  0  THEN  Auto)))xxx

---

Home Index