### Nuprl Lemma : compact-proper-interval-near-member

`∀J:Interval`
`  (icompact(J)`
`  `` iproper(J)`
`  `` (∀x:ℝ. ((x ∈ J) `` (∀r:ℝ. ((r0 < r) `` (∃y:ℝ. ((y ∈ J) ∧ (|y - x| ≤ r) ∧ (r0 < |y - x|))))))))`

Proof

Definitions occuring in Statement :  icompact: `icompact(I)` i-member: `r ∈ I` iproper: `iproper(I)` interval: `Interval` rleq: `x ≤ y` rless: `x < y` rabs: `|x|` rsub: `x - y` int-to-real: `r(n)` real: `ℝ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` interval: `Interval` iproper: `iproper(I)` icompact: `icompact(I)` 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` i-member: `r ∈ I` right-endpoint: `right-endpoint(I)` left-endpoint: `left-endpoint(I)` endpoints: `endpoints(I)` pi1: `fst(t)` pi2: `snd(t)` implies: `P `` Q` and: `P ∧ Q` cand: `A c∧ B` true: `True` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` false: `False` or: `P ∨ Q` iff: `P `⇐⇒` Q` uimplies: `b supposing a` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` not: `¬A` top: `Top` uiff: `uiff(P;Q)` squash: `↓T` subtype_rel: `A ⊆r B` guard: `{T}` rev_implies: `P `` Q` rev_uimplies: `rev_uimplies(P;Q)` rge: `x ≥ y` rsub: `x - y`
Lemmas referenced :  rless_wf int-to-real_wf real_wf rleq_wf true_wf exists_wf false_wf interval_wf rless-cases rmin_strict_ub rsub_wf rless-implies-rless real_term_polynomial itermSubtract_wf itermVar_wf itermConstant_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_var_lemma req-iff-rsub-is-0 itermMinus_wf rmin_wf real_term_value_minus_lemma rminus_wf rabs_wf squash_wf rabs-rminus iff_weakening_equal rmin-rleq rleq_weakening_rless rleq_functionality rabs_functionality req_weakening rless_functionality rabs-of-nonneg radd-preserves-rleq radd_wf itermAdd_wf real_term_value_add_lemma rmin_functionality rleq_weakening_equal rleq_functionality_wrt_implies trivial-rsub-rleq rmul_wf uiff_transitivity req_transitivity radd_functionality rminus-as-rmul req_inversion rmul-identity1 rmul-distrib2 radd-assoc rmul_functionality radd-int rmul-zero-both radd-zero-both
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin unionElimination sqequalRule rename cut hypothesis independent_functionElimination natural_numberEquality independent_pairFormation because_Cache introduction extract_by_obid isectElimination hypothesisEquality productEquality functionEquality lambdaEquality voidElimination dependent_functionElimination independent_isectElimination computeAll int_eqEquality intEquality isect_memberEquality voidEquality dependent_pairFormation addLevel applyEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed universeEquality addEquality minusEquality lemma_by_obid

Latex:
\mforall{}J:Interval
(icompact(J)
{}\mRightarrow{}  iproper(J)
{}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  ((x  \mmember{}  J)  {}\mRightarrow{}  (\mforall{}r:\mBbbR{}.  ((r0  <  r)  {}\mRightarrow{}  (\mexists{}y:\mBbbR{}.  ((y  \mmember{}  J)  \mwedge{}  (|y  -  x|  \mleq{}  r)  \mwedge{}  (r0  <  |y  -  x|))))))))

Date html generated: 2017_10_03-AM-09_35_11
Last ObjectModification: 2017_07_28-AM-07_52_47

Theory : reals

Home Index