Nuprl Definition : weak-continuity
weak-continuity(T;V) ==
∀F:(ℕ ⟶ T) ⟶ V. ∀f:ℕ ⟶ T. (↓∃n:ℕ. ∀g:ℕ ⟶ T. ((∀i:ℕn. ((f i) = (g i) ∈ T)) ⇒ ((F f) = (F g) ∈ V)))
Definitions occuring in Statement :
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
squash: ↓T,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
nat: ℕ,
implies: P ⇒ Q,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
equal: s = t ∈ T,
apply: f a
FDL editor aliases :
weak-continuity
Latex:
weak-continuity(T;V) ==
\mforall{}F:(\mBbbN{} {}\mrightarrow{} T) {}\mrightarrow{} V. \mforall{}f:\mBbbN{} {}\mrightarrow{} T. (\mdownarrow{}\mexists{}n:\mBbbN{}. \mforall{}g:\mBbbN{} {}\mrightarrow{} T. ((\mforall{}i:\mBbbN{}n. ((f i) = (g i))) {}\mRightarrow{} ((F f) = (F g))))
Date html generated:
2016_05_15-PM-01_46_35
Last ObjectModification:
2015_09_23-AM-07_37_06
Theory : basic
Home
Index