Nuprl Definition : proper-real-continuity
proper-real-continuity() ==
∀a,b:ℝ.
((a < b)
⇒ (∀f:[a, b] ⟶ℝ. ∀n:ℕ+.
(∃d:{ℝ| ((r0 < d)
∧ (∀x,y:ℝ. ((x ∈ [a, b]) ⇒ (y ∈ [a, b]) ⇒ (|x - y| ≤ d) ⇒ (|(f x) - f y| ≤ (r1/r(n))))))})))
Definitions occuring in Statement :
rfun: I ⟶ℝ,
rccint: [l, u],
i-member: r ∈ I,
rdiv: (x/y),
rleq: x ≤ y,
rless: x < y,
rabs: |x|,
rsub: x - y,
int-to-real: r(n),
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
natural_number: $n
Definitions occuring in definition :
rfun: I ⟶ℝ,
nat_plus: ℕ+,
sq_exists: ∃x:{A| B[x]},
and: P ∧ Q,
rless: x < y,
all: ∀x:A. B[x],
real: ℝ,
i-member: r ∈ I,
rccint: [l, u],
implies: P ⇒ Q,
rleq: x ≤ y,
rabs: |x|,
rsub: x - y,
apply: f a,
rdiv: (x/y),
natural_number: $n,
int-to-real: r(n)
FDL editor aliases :
proper-real-continuity
Latex:
proper-real-continuity() ==
\mforall{}a,b:\mBbbR{}.
((a < b)
{}\mRightarrow{} (\mforall{}f:[a, b] {}\mrightarrow{}\mBbbR{}. \mforall{}n:\mBbbN{}\msupplus{}.
(\mexists{}d:\{\mBbbR{}| ((r0 < d)
\mwedge{} (\mforall{}x,y:\mBbbR{}.
((x \mmember{} [a, b])
{}\mRightarrow{} (y \mmember{} [a, b])
{}\mRightarrow{} (|x - y| \mleq{} d)
{}\mRightarrow{} (|(f x) - f y| \mleq{} (r1/r(n))))))\})))
Date html generated:
2016_05_18-AM-10_52_16
Last ObjectModification:
2015_09_23-AM-09_17_42
Theory : reals
Home
Index