---

Step * of Lemma rv-le_witness

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].  (X ≤ Y ⇒ (λs.Ax ∈ 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))) }

1
1. p : ℚ List
2. Σ0 ≤ i < ||p||. p[i] = 1 ∈ ℚ
3. (∀q∈p.0 ≤ q)
4. n : ℕ
5. X : (ℕn ─→ ℕ||p||) ─→ ℚ
6. Y : (ℕn ─→ ℕ||p||) ─→ ℚ
7. ∀s:ℕn ─→ Outcome. ((X s) ≤ (Y s))@i
8. s : ℕn ─→ Outcome@i
⊢ Ax ∈ (X s) ≤ (Y s)

---

Latex:


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


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