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