Nuprl Definition : discontinuous
discontinuous(f;x) ==
  ∃epsilon:{e:ℝ| r0 < e} . ∀delta:{e:ℝ| r0 < e} . ∃y:ℝ. ((|x - y| < delta) ∧ (epsilon < |(f x) - f y|))
Definitions occuring in Statement : 
rless: x < y
, 
rabs: |x|
, 
rsub: x - y
, 
int-to-real: r(n)
, 
real: ℝ
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
and: P ∧ Q
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
natural_number: $n
Definitions occuring in definition : 
all: ∀x:A. B[x]
, 
set: {x:A| B[x]} 
, 
int-to-real: r(n)
, 
natural_number: $n
, 
exists: ∃x:A. B[x]
, 
real: ℝ
, 
and: P ∧ Q
, 
rless: x < y
, 
rabs: |x|
, 
rsub: x - y
, 
apply: f a
FDL editor aliases : 
discontinuous
Latex:
discontinuous(f;x)  ==
    \mexists{}epsilon:\{e:\mBbbR{}|  r0  <  e\} 
      \mforall{}delta:\{e:\mBbbR{}|  r0  <  e\}  .  \mexists{}y:\mBbbR{}.  ((|x  -  y|  <  delta)  \mwedge{}  (epsilon  <  |(f  x)  -  f  y|))
Date html generated:
2016_05_18-AM-11_13_26
Last ObjectModification:
2015_09_23-AM-09_18_42
Theory : reals
Home
Index