---

Step * of Lemma p-measure-le_wf

∀[p:FinProbSpace]. ∀[q:ℚ]. ∀[C:p-open(p)].  (measure(C) ≤ q ∈ ℙ)
BY
{ (Unfold `p-measure-le` 0 THEN Auto) }

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[q:\mBbbQ{}].  \mforall{}[C:p-open(p)].    (measure(C)  \mleq{}  q  \mmember{}  \mBbbP{})


By

(Unfold  `p-measure-le`  0  THEN  Auto)

---

Home Index