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