Nuprl Definition : p-measure-le
measure(C) ≤ q == ∀n:ℕ. E(n;λs.(C <n, s>)) < q
Definitions occuring in Statement :
expectation: E(n;F),
nat: ℕ,
all: ∀x:A. B[x],
apply: f a,
lambda: λx.A[x],
pair: <a, b>
Definitions :
all: ∀x:A. B[x],
nat: ℕ,
qless: Error :qless,
expectation: E(n;F),
lambda: λx.A[x],
apply: f a,
pair: <a, b>
FDL editor aliases :
p-measure-le
measure(C) \mleq{} q == \mforall{}n:\mBbbN{}. E(n;\mlambda{}s.(C <n, s>)) < q
Date html generated:
2015_07_17-AM-07_59_58
Last ObjectModification:
2008_02_27-PM-05_49_27
Home
Index