---

Step * of Lemma expectation-rv-const

∀[p:FinProbSpace]. ∀[a:ℚ]. ∀[n:ℕ].  (E(n;a) = a ∈ ℚ)
BY
{ (Auto⋅ THEN BLemma `expectation-constant` THEN Auto THEN RepUR ``rv-const`` 0 THEN Auto) }

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[a:\mBbbQ{}].  \mforall{}[n:\mBbbN{}].    (E(n;a)  =  a)


By

(Auto\mcdot{}  THEN  BLemma  `expectation-constant`  THEN  Auto  THEN  RepUR  ``rv-const``  0  THEN  Auto)

---

Home Index