---

Step * of Lemma rv-le_wf

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].  (X ≤ Y ∈ ℙ)
BY
{ (Unfolds ``rv-le random-variable`` 0
   THEN Auto
   THEN Try ((Fold `p-outcome` 0 THEN Auto))
   THEN Try ((DVar `p' THEN Auto))) }

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X,Y:RandomVariable(p;n)].    (X  \mleq{}  Y  \mmember{}  \mBbbP{})


By

(Unfolds  ``rv-le  random-variable``  0
  THEN  Auto
  THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto))
  THEN  Try  ((DVar  `p'  THEN  Auto)))

---

Home Index