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
Definitions :
set: {x:A| B[x]} ,
product: x:A × B[x],
function: x:A ─→ B[x],
p-outcome: Outcome,
nat: ℕ,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
le: A ≤ B,
apply: f a,
pair: <a, b>
FDL editor aliases :
p-open
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:
2015_07_17-AM-07_59_53
Last ObjectModification:
2008_02_27-PM-05_49_21
Home
Index