Nuprl Definition : neighbourhood-function-nat
K0(G) == (∀f:ℕ ⟶ ℕ. ∃n:ℕ. (↑isl(G f^(n)))) ∧ (∀f,g:finite-nat-seq(). ((↑isl(G f)) ⇒ ((G f) = (G f**g) ∈ (ℕ?))))
Definitions occuring in Statement :
append-finite-nat-seq: f**g,
mk-finite-nat-seq: f^(n),
finite-nat-seq: finite-nat-seq(),
nat: ℕ,
assert: ↑b,
isl: isl(x),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
unit: Unit,
apply: f a,
function: x:A ⟶ B[x],
union: left + right,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
function: x:A ⟶ B[x],
exists: ∃x:A. B[x],
mk-finite-nat-seq: f^(n),
all: ∀x:A. B[x],
finite-nat-seq: finite-nat-seq(),
implies: P ⇒ Q,
assert: ↑b,
isl: isl(x),
equal: s = t ∈ T,
union: left + right,
nat: ℕ,
unit: Unit,
apply: f a,
append-finite-nat-seq: f**g
FDL editor aliases :
neighbourhood-function-nat
Latex:
K0(G) ==
(\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mexists{}n:\mBbbN{}. (\muparrow{}isl(G f\^{}(n)))) \mwedge{} (\mforall{}f,g:finite-nat-seq(). ((\muparrow{}isl(G f)) {}\mRightarrow{} ((G f) = (G f**g))))
Date html generated:
2016_05_14-PM-09_54_40
Last ObjectModification:
2016_01_15-AM-09_05_55
Theory : continuity
Home
Index