Nuprl Definition : m-ptwise-cont
PtwiseCONT(f:X ⟶ Y) ==
  ∀x:X. ∀k:ℕ+.  ∃delta:{d:ℝ| r0 < d} . ∀y:X. ((mdist(dx;x;y) ≤ delta) 
⇒ (mdist(dy;f x;f y) ≤ (r1/r(k))))
Definitions occuring in Statement : 
mdist: mdist(d;x;y)
, 
rdiv: (x/y)
, 
rleq: x ≤ y
, 
rless: x < y
, 
int-to-real: r(n)
, 
real: ℝ
, 
nat_plus: ℕ+
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
implies: P 
⇒ Q
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
natural_number: $n
FDL editor aliases : 
m-ptwise-cont
Latex:
PtwiseCONT(f:X  {}\mrightarrow{}  Y)  ==
    \mforall{}x:X.  \mforall{}k:\mBbbN{}\msupplus{}.
        \mexists{}delta:\{d:\mBbbR{}|  r0  <  d\}  .  \mforall{}y:X.  ((mdist(dx;x;y)  \mleq{}  delta)  {}\mRightarrow{}  (mdist(dy;f  x;f  y)  \mleq{}  (r1/r(k))))
Date html generated:
2020_05_20-AM-11_48_07
Last ObjectModification:
2019_11_08-AM-09_59_38
Theory : reals
Home
Index