Nuprl Definition : nullset
nullset(p;S) == ∀q:{q:ℚ| 0 < q} . ∃C:p-open(p). ((∀s:ℕ ⟶ Outcome. ((S s)
⇒ s ∈ C)) ∧ measure(C) ≤ q)
Definitions occuring in Statement :
p-measure-le: measure(C) ≤ q
,
p-open-member: s ∈ C
,
p-open: p-open(p)
,
p-outcome: Outcome
,
qless: r < s
,
rationals: ℚ
,
nat: ℕ
,
all: ∀x:A. B[x]
,
exists: ∃x:A. B[x]
,
implies: P
⇒ Q
,
and: P ∧ Q
,
set: {x:A| B[x]}
,
apply: f a
,
function: x:A ⟶ B[x]
,
natural_number: $n
FDL editor aliases :
nullset
Latex:
nullset(p;S) ==
\mforall{}q:\{q:\mBbbQ{}| 0 < q\} . \mexists{}C:p-open(p). ((\mforall{}s:\mBbbN{} {}\mrightarrow{} Outcome. ((S s) {}\mRightarrow{} s \mmember{} C)) \mwedge{} measure(C) \mleq{} q)
Date html generated:
2016_05_15-PM-11_49_58
Last ObjectModification:
2008_02_27-PM-05_49_43
Theory : randomness
Home
Index