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