---

Step * of Lemma expectation_wf

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)].  (E(n;X) ∈ ℚ)
BY
{ (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))) }

---

Latex:


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


By

(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)))

---

Home Index