---

Step * 1 1 of Lemma expectation-constant


1. p : FinProbSpace
2. a : ℚ
3. n : ℤ
⊢ ∀X:RandomVariable(p;0). ((∀s:ℕ0 ⟶ Outcome. ((X s) = a ∈ ℚ)) ⇒ ((X null) = a ∈ ℚ))
BY
{ ((Unfold `random-variable` 0 THEN Auto) THEN BHyp -1  THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  p  :  FinProbSpace
2.  a  :  \mBbbQ{}
3.  n  :  \mBbbZ{}
\mvdash{}  \mforall{}X:RandomVariable(p;0).  ((\mforall{}s:\mBbbN{}0  {}\mrightarrow{}  Outcome.  ((X  s)  =  a))  {}\mRightarrow{}  ((X  null)  =  a))


By

---

Latex:
((Unfold  `random-variable`  0  THEN  Auto)  THEN  BHyp  -1    THEN  Auto)\mcdot{}

---

Home Index