### 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