Nuprl Definition : locally-non-constant

locally-non-constant(f;a;b;c) ==  ∀u,v:ℝ.  ((a ≤ u)  (u < v)  (v ≤ b)  (∃z:ℝ((u ≤ z) ∧ (z ≤ v) ∧ f(z) ≠ c)))



Definitions occuring in Statement :  r-ap: f(x) rneq: x ≠ y rleq: x ≤ y rless: x < y real: all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q
Definitions occuring in definition :  all: x:A. B[x] rless: x < y implies:  Q exists: x:A. B[x] real: and: P ∧ Q rleq: x ≤ y rneq: x ≠ y r-ap: f(x)
FDL editor aliases :  locally-non-constant

Latex:
locally-non-constant(f;a;b;c)  ==
    \mforall{}u,v:\mBbbR{}.    ((a  \mleq{}  u)  {}\mRightarrow{}  (u  <  v)  {}\mRightarrow{}  (v  \mleq{}  b)  {}\mRightarrow{}  (\mexists{}z:\mBbbR{}.  ((u  \mleq{}  z)  \mwedge{}  (z  \mleq{}  v)  \mwedge{}  f(z)  \mneq{}  c)))



Date html generated: 2016_05_18-AM-09_23_47
Last ObjectModification: 2015_09_23-AM-09_10_56

Theory : reals


Home Index