Nuprl Definition : strong-continuity3
strong-continuity3(T;F) ==
∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
∀f:ℕ ⟶ T. ∃n:ℕ. (((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
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 :
nat: ℕ,
equal: s = t ∈ T,
apply: f a,
isl: isl(x),
assert: ↑b,
implies: P ⇒ Q,
all: ∀x:A. B[x],
inl: inl x,
unit: Unit,
union: left + right,
and: P ∧ Q,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
natural_number: $n,
int_seg: {i..j-}
FDL editor aliases :
strong-continuity3
Latex:
strong-continuity3(T;F) ==
\mexists{}M:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} (\mBbbN{}?)
\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 = n))))
Date html generated:
2016_12_12-AM-09_22_37
Last ObjectModification:
2016_11_22-AM-11_41_11
Theory : continuity
Home
Index