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