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,
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,
rationals: ℚ
Definitions :
set: {x:A| B[x]} ,
rationals: ℚ,
qless: Error :qless,
natural_number: $n,
exists: ∃x:A. B[x],
p-open: p-open(p),
and: P ∧ Q,
all: ∀x:A. B[x],
function: x:A ─→ B[x],
nat: ℕ,
p-outcome: Outcome,
implies: P ⇒ Q,
apply: f a,
p-open-member: s ∈ C,
p-measure-le: measure(C) ≤ q
FDL editor aliases :
nullset
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:
2015_07_17-AM-08_00_50
Last ObjectModification:
2008_02_27-PM-05_49_43
Home
Index