Nuprl Definition : strong-continuity4
strong-continuity4(T;F) ==
∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕn?)
∀f:ℕ ⟶ T. ∃n:ℕ. (((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ ((M m f) = (inl (F f)) ∈ (ℕ?)))))
Definitions occuring in Statement :
int_seg: {i..j-},
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],
inl: inl x,
union: left + right,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
apply: f a,
inl: inl x,
unit: Unit,
nat: ℕ,
union: left + right,
equal: s = t ∈ T,
isl: isl(x),
assert: ↑b,
implies: P ⇒ Q,
all: ∀x:A. B[x],
and: P ∧ Q,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
natural_number: $n,
int_seg: {i..j-}
FDL editor aliases :
strong-continuity4
Latex:
strong-continuity4(T;F) ==
\mexists{}M:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} (\mBbbN{}n?)
\mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mexists{}n:\mBbbN{}. (((M n f) = (inl (F f))) \mwedge{} (\mforall{}m:\mBbbN{}. ((\muparrow{}isl(M m f)) {}\mRightarrow{} ((M m f) = (inl (F f))))))
Date html generated:
2017_09_29-PM-06_05_20
Last ObjectModification:
2017_09_03-PM-10_12_11
Theory : continuity
Home
Index