---

Step * of Lemma rv-add_wf

No Annotations
∀[k:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(k;n)].  (X + Y ∈ RandomVariable(k;n))
BY
{ (Intros THEN Unhide THEN All (Unfolds ``finite-prob-space random-variable rv-add``)⋅ THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X,Y:RandomVariable(k;n)].    (X  +  Y  \mmember{}  RandomVariable(k;n))


By

---

Latex:
(Intros  THEN  Unhide  THEN  All  (Unfolds  ``finite-prob-space  random-variable  rv-add``)\mcdot{}  THEN  Auto)

---

Home Index