Nuprl Definition : basic-strong-continuity
basic-strong-continuity(T;F) ==
∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ)) [(∀f:ℕ ⟶ T
((∃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 :
int_seg: {i..j-},
nat: ℕ,
b-union: A ⋃ B,
uimplies: b supposing a,
isint: isint def,
le: A ≤ B,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
false: False,
true: True,
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
sq_exists: ∃x:A [B[x]],
int_seg: {i..j-},
natural_number: $n,
b-union: A ⋃ B,
product: x:A × B[x],
function: x:A ⟶ B[x],
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 :
basic-strong-continuity
Latex:
basic-strong-continuity(T;F) ==
\mexists{}M:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} (\mBbbN{} \mcup{} (\mBbbN{} \mtimes{} \mBbbN{})) [(\mforall{}f:\mBbbN{} {}\mrightarrow{} T
((\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_11
Last ObjectModification:
2019_02_11-AM-11_18_07
Theory : continuity
Home
Index