Nuprl Definition : p-open
p-open(p) == {C:(n:ℕ × (ℕn ⟶ Outcome)) ⟶ ℕ2| ∀s:ℕ ⟶ Outcome. ∀j:ℕ. ∀i:ℕj. ((C <i, s>) ≤ (C <j, s>))}
Definitions occuring in Statement :
p-outcome: Outcome,
int_seg: {i..j-},
nat: ℕ,
le: A ≤ B,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
pair: <a, b>,
product: x:A × B[x],
natural_number: $n
FDL editor aliases :
p-open
Latex:
p-open(p) ==
\{C:(n:\mBbbN{} \mtimes{} (\mBbbN{}n {}\mrightarrow{} Outcome)) {}\mrightarrow{} \mBbbN{}2| \mforall{}s:\mBbbN{} {}\mrightarrow{} Outcome. \mforall{}j:\mBbbN{}. \mforall{}i:\mBbbN{}j. ((C <i, s>) \mleq{} (C <j, s>))\}
Date html generated:
2016_05_15-PM-11_48_41
Last ObjectModification:
2008_02_27-PM-05_49_21
Theory : randomness
Home
Index