---

Step * of Lemma rv-qle_wf

∀[k:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(k;n)].  (X ≤ Y ∈ RandomVariable(k;n))
BY
{ (Unfolds ``random-variable finite-prob-space rv-qle`` 0 THEN Auto)⋅ }

---

Latex:


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


By

(Unfolds  ``random-variable  finite-prob-space  rv-qle``  0  THEN  Auto)\mcdot{}

---

Home Index