---

Step * of Lemma p-outcome_wf

∀[p:FinProbSpace]. (Outcome ∈ Type)
BY
{ (Unfolds ``finite-prob-space p-outcome`` 0 THEN Auto) }

---

Latex:


\mforall{}[p:FinProbSpace].  (Outcome  \mmember{}  Type)


By

(Unfolds  ``finite-prob-space  p-outcome``  0  THEN  Auto)

---

Home Index