Step * of Lemma nullset_wf

[p:FinProbSpace]. ∀[S:(ℕ ⟶ Outcome) ⟶ ℙ].  (nullset(p;S) ∈ ℙ)
BY
(Unfold `nullset` THEN Auto) }


Latex:


Latex:
\mforall{}[p:FinProbSpace].  \mforall{}[S:(\mBbbN{}  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbP{}].    (nullset(p;S)  \mmember{}  \mBbbP{})


By


Latex:
(Unfold  `nullset`  0  THEN  Auto)




Home Index