Step
*
of Lemma
nullset_wf
∀[p:FinProbSpace]. ∀[S:(ℕ ─→ Outcome) ─→ ℙ].  (nullset(p;S) ∈ ℙ)
BY
{ (Unfold `nullset` 0 THEN Auto) }
Latex:
\mforall{}[p:FinProbSpace].  \mforall{}[S:(\mBbbN{}  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbP{}].    (nullset(p;S)  \mmember{}  \mBbbP{})
By
(Unfold  `nullset`  0  THEN  Auto)
Home
Index