---

Step * of Lemma nullset-monotone

∀p:FinProbSpace. ∀[P,Q:(ℕ ─→ Outcome) ─→ ℙ].  ((∀s:ℕ ─→ Outcome. (Q[s] ⇒ P[s])) ⇒ nullset(p;P) ⇒ nullset(p;Q))
BY
{ (Auto THEN RepeatFor 6 (ParallelLast) THEN BackThruSomeHyp THEN Auto) }

---

Latex:


\mforall{}p:FinProbSpace
    \mforall{}[P,Q:(\mBbbN{}  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  (Q[s]  {}\mRightarrow{}  P[s]))  {}\mRightarrow{}  nullset(p;P)  {}\mRightarrow{}  nullset(p;Q))


By

(Auto  THEN  RepeatFor  6  (ParallelLast)  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index