Nuprl Definition : weak-continuity-skolem
weak-continuity-skolem(T;F) == ∃M:(ℕ ⟶ T) ⟶ ℕ. ∀f,g:ℕ ⟶ T. ((f = g ∈ (ℕM f ⟶ T)) ⇒ ((F f) = (F g) ∈ ℕ))
Definitions occuring in Statement :
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
apply: f a,
nat: ℕ,
equal: s = t ∈ T,
natural_number: $n,
int_seg: {i..j-},
function: x:A ⟶ B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
exists: ∃x:A. B[x]
FDL editor aliases :
weak-continuity-skolem
Latex:
weak-continuity-skolem(T;F) == \mexists{}M:(\mBbbN{} {}\mrightarrow{} T) {}\mrightarrow{} \mBbbN{}. \mforall{}f,g:\mBbbN{} {}\mrightarrow{} T. ((f = g) {}\mRightarrow{} ((F f) = (F g)))
Date html generated:
2016_12_12-AM-09_22_54
Last ObjectModification:
2016_11_22-PM-00_01_54
Theory : continuity
Home
Index