---

Step * of Lemma p-open-measure-one_wf

∀[p:FinProbSpace]. ∀[C:p-open(p)].  (measure(C) = 1 ∈ ℙ)
BY
{ (Unfold `p-open-measure-one` 0 THEN Auto) }

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[C:p-open(p)].    (measure(C)  =  1  \mmember{}  \mBbbP{})


By

(Unfold  `p-open-measure-one`  0  THEN  Auto)

---

Home Index