Nuprl Definition : bsc-body
bsc-body(F;M;f) ==
(∃n:ℕ. ((M n f) = (F f) ∈ ℕ))
∧ (∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer)
∧ (∀n,m:ℕ. ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer))
Definitions occuring in Statement :
nat: ℕ,
uimplies: b supposing a,
isint: isint def,
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
false: False,
true: True,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
and: P ∧ Q,
uimplies: b supposing a,
equal: s = t ∈ T,
all: ∀x:A. B[x],
nat: ℕ,
le: A ≤ B,
implies: P ⇒ Q,
isint: isint def,
apply: f a,
true: True,
false: False
FDL editor aliases :
bsc-body
Latex:
bsc-body(F;M;f) ==
(\mexists{}n:\mBbbN{}. ((M n f) = (F f)))
\mwedge{} (\mforall{}n:\mBbbN{}. (M n f) = (F f) supposing M n f is an integer)
\mwedge{} (\mforall{}n,m:\mBbbN{}. ((n \mleq{} m) {}\mRightarrow{} M n f is an integer {}\mRightarrow{} M m f is an integer))
Date html generated:
2019_06_20-PM-02_50_05
Last ObjectModification:
2019_02_11-AM-11_16_37
Theory : continuity
Home
Index