Nuprl Definition : locally-non-constant-rational
locally-non-constant-rational(f;a;b;c) ==
∀u,v:ℝ. ((a ≤ u) ⇒ (u < v) ⇒ (v ≤ b) ⇒ (∃n:ℕ+. ∃z:ℤ. ((u ≤ (r(z))/n) ∧ ((r(z))/n ≤ v) ∧ f((r(z))/n) ≠ c)))
Definitions occuring in Statement :
r-ap: f(x),
rneq: x ≠ y,
rleq: x ≤ y,
rless: x < y,
int-rdiv: (a)/k1,
int-to-real: r(n),
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
int: ℤ
Definitions occuring in definition :
all: ∀x:A. B[x],
real: ℝ,
rless: x < y,
implies: P ⇒ Q,
nat_plus: ℕ+,
exists: ∃x:A. B[x],
int: ℤ,
and: P ∧ Q,
rleq: x ≤ y,
rneq: x ≠ y,
r-ap: f(x),
int-rdiv: (a)/k1,
int-to-real: r(n)
FDL editor aliases :
locally-non-constant-rational
Latex:
locally-non-constant-rational(f;a;b;c) ==
\mforall{}u,v:\mBbbR{}.
((a \mleq{} u)
{}\mRightarrow{} (u < v)
{}\mRightarrow{} (v \mleq{} b)
{}\mRightarrow{} (\mexists{}n:\mBbbN{}\msupplus{}. \mexists{}z:\mBbbZ{}. ((u \mleq{} (r(z))/n) \mwedge{} ((r(z))/n \mleq{} v) \mwedge{} f((r(z))/n) \mneq{} c)))
Date html generated:
2016_05_18-AM-09_24_14
Last ObjectModification:
2015_09_23-AM-09_11_03
Theory : reals
Home
Index