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: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
rless: x < y,
implies: P ⇒ 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