Nuprl Lemma : function-on-compact
∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:[a, b] ⟶ℝ.
((∀x,y:{t:ℝ| t ∈ [a, b]} . ((x = y) ⇒ (f[x] = f[y])))
⇒ (∀n:ℕ+
(∃d:ℝ [((r0 < d)
∧ (∀x,y:ℝ. ((x ∈ [a, b]) ⇒ (y ∈ [a, b]) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))])))
Proof
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,
req: x = y,
int-to-real: r(n),
real: ℝ,
nat_plus: ℕ+,
so_apply: x[s],
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
rfun: I ⟶ℝ,
so_apply: x[s],
so_lambda: λ2x.t[x],
top: Top,
sq_stable: SqStable(P),
iff: P ⇐⇒ Q,
prop: ℙ,
and: P ∧ Q,
true: True,
less_than': less_than'(a;b),
squash: ↓T,
less_than: a < b,
nat_plus: ℕ+,
rccint: [l, u],
i-approx: i-approx(I;n),
continuous: f[x] continuous for x ∈ I,
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
rleq_wf,
set_wf,
rfun_wf,
req_wf,
i-member_wf,
real_wf,
all_wf,
nat_plus_wf,
member_rccint_lemma,
icompact_wf,
sq_stable__rleq,
rccint-icompact,
less_than_wf,
rccint_wf,
function-is-continuous
Rules used in proof :
applyEquality,
functionEquality,
lambdaEquality,
setEquality,
voidEquality,
voidElimination,
isect_memberEquality,
imageElimination,
productElimination,
baseClosed,
imageMemberEquality,
independent_pairFormation,
natural_numberEquality,
dependent_set_memberEquality,
sqequalRule,
independent_functionElimination,
hypothesis,
because_Cache,
rename,
setElimination,
hypothesisEquality,
isectElimination,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}a:\mBbbR{}. \mforall{}b:\{b:\mBbbR{}| a \mleq{} b\} . \mforall{}f:[a, b] {}\mrightarrow{}\mBbbR{}.
((\mforall{}x,y:\{t:\mBbbR{}| t \mmember{} [a, b]\} . ((x = y) {}\mRightarrow{} (f[x] = f[y])))
{}\mRightarrow{} (\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:
2018_07_29-AM-09_40_44
Last ObjectModification:
2018_06_22-PM-04_47_33
Theory : reals
Home
Index