### 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