Nuprl Lemma : i-approx-rep
∀I:Interval. ∀n:ℕ+. ∀r:ℝ. ((r ∈ i-approx(I;n)) ⇒ (∃a,b:ℝ. ((a ≤ b) ∧ (i-approx(I;n) = [a, b] ∈ Interval))))
Proof
Definitions occuring in Statement :
i-approx: i-approx(I;n),
rccint: [l, u],
i-member: r ∈ I,
interval: Interval,
rleq: x ≤ y,
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
implies: P ⇒ Q,
prop: ℙ,
uall: ∀[x:A]. B[x],
exists: ∃x:A. B[x],
uimplies: b supposing a,
and: P ∧ Q,
cand: A c∧ B,
so_lambda: λ2x.t[x],
so_apply: x[s],
icompact: icompact(I),
interval: Interval,
i-finite: i-finite(I),
i-closed: i-closed(I),
i-nonvoid: i-nonvoid(I),
isl: isl(x),
outl: outl(x),
bnot: ¬bb,
ifthenelse: if b then t else f fi ,
btrue: tt,
assert: ↑b,
bor: p ∨bq,
bfalse: ff,
false: False,
top: Top,
rccint: [l, u],
squash: ↓T,
true: True
Lemmas referenced :
i-approx-compact,
i-member_wf,
i-approx_wf,
real_wf,
nat_plus_wf,
interval_wf,
equal_wf,
left-endpoint_wf,
right-endpoint_wf,
rleq_wf,
rccint_wf,
exists_wf,
icompact_wf,
icompact-endpoints-rleq,
squash_wf,
true_wf,
left_endpoint_rccint_lemma,
right_endpoint_rccint_lemma
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
independent_functionElimination,
isectElimination,
equalityTransitivity,
equalitySymmetry,
dependent_pairFormation,
independent_isectElimination,
because_Cache,
independent_pairFormation,
productEquality,
sqequalRule,
lambdaEquality,
productElimination,
unionElimination,
voidElimination,
applyEquality,
imageElimination,
isect_memberEquality,
voidEquality,
natural_numberEquality,
imageMemberEquality,
baseClosed
Latex:
\mforall{}I:Interval. \mforall{}n:\mBbbN{}\msupplus{}. \mforall{}r:\mBbbR{}. ((r \mmember{} i-approx(I;n)) {}\mRightarrow{} (\mexists{}a,b:\mBbbR{}. ((a \mleq{} b) \mwedge{} (i-approx(I;n) = [a, b]))))
Date html generated:
2017_10_03-AM-09_34_39
Last ObjectModification:
2017_07_28-AM-07_52_25
Theory : reals
Home
Index