Nuprl Definition : p-open-measure-one
measure(C) = 1 == ∀m:ℕ+. ∃n:ℕ. ((1 - (1/m)) ≤ E(n;λs.(C <n, s>)))
Definitions occuring in Statement :
expectation: E(n;F),
nat_plus: ℕ+,
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
natural_number: $n,
qsub: r - s,
qdiv: (r/s)
Definitions :
all: ∀x:A. B[x],
nat_plus: ℕ+,
exists: ∃x:A. B[x],
nat: ℕ,
qle: Error :qle,
qsub: r - s,
qdiv: (r/s),
natural_number: $n,
expectation: E(n;F),
lambda: λx.A[x],
apply: f a,
pair: <a, b>
FDL editor aliases :
p-open-measure-one
measure(C) = 1 == \mforall{}m:\mBbbN{}\msupplus{}. \mexists{}n:\mBbbN{}. ((1 - (1/m)) \mleq{} E(n;\mlambda{}s.(C <n, s>)))
Date html generated:
2015_07_17-AM-08_00_09
Last ObjectModification:
2008_02_27-PM-05_49_31
Home
Index