Nuprl Lemma : closures-meet-sq-ext

[P,Q:ℝ ⟶ ℙ].
  ((∃a:{a:ℝa} (∃b:ℝ [((Q b) ∧ (a ≤ b))]))
   (∃c:{c:ℝ(r0 ≤ c) ∧ (c < r1)} 
       ∀a:{a:ℝa} . ∀b:{b:ℝ(Q b) ∧ (a ≤ b)} .
         ∃a':{a':ℝa'} (∃b':{b':ℝ(Q b') ∧ (a' ≤ b')}  [((a ≤ a') ∧ (b' ≤ b) ∧ ((b' a') ≤ ((b a) c)))]))
   (∃y:ℝ(y ∈ closure(λz.(↓z)) ∧ y ∈ closure(λz.(↓z)))))


Proof




Definitions occuring in Statement :  member-closure: y ∈ closure(A) rleq: x ≤ y rless: x < y rsub: y rmul: b int-to-real: r(n) real: uall: [x:A]. B[x] prop: all: x:A. B[x] sq_exists: x:A [B[x]] exists: x:A. B[x] squash: T implies:  Q and: P ∧ Q set: {x:A| B[x]}  apply: a lambda: λx.A[x] function: x:A ⟶ B[x] natural_number: $n
Definitions unfolded in proof :  member: t ∈ T pi1: fst(t) so_apply: x[s] so_lambda: λ2x.t[x] pi2: snd(t) subtract: m rabs: |x| rmax: rmax(x;y) imax: imax(a;b) ifthenelse: if then else fi  le_int: i ≤j bnot: ¬bb lt_int: i <j btrue: tt it: bfalse: ff canonical-bound: canonical-bound(r) divide: n ÷ m absval: |i| int-to-real: r(n) let: let closures-meet-sq common-limit-squeeze-ext sq_stable__rleq converges-to_functionality rmul-limit constant-limit req_weakening rpowers-converge-ext rless_functionality sq_stable__rless integer-bound converges-implies-bounded rleq_functionality_wrt_implies sq-all-large-and uall: [x:A]. B[x] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] top: Top uimplies: supposing a so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] strict4: strict4(F) and: P ∧ Q all: x:A. B[x] implies:  Q has-value: (a)↓ prop: or: P ∨ Q squash: T primrec: primrec(n;b;c) primtailrec: primtailrec(n;i;b;f) false: False
Lemmas referenced :  closures-meet-sq lifting-strict-spread istype-void strict4-apply strict4-spread value-type-has-value int-value-type has-value_wf_base istype-base is-exception_wf istype-universe strict4-divide lifting-strict-callbyvalue lifting-strict-decide strict4-decide cbv_sqequal lifting-strict-less exception-not-value common-limit-squeeze-ext sq_stable__rleq converges-to_functionality rmul-limit constant-limit req_weakening rpowers-converge-ext rless_functionality sq_stable__rless integer-bound converges-implies-bounded rleq_functionality_wrt_implies sq-all-large-and
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry isectElimination baseClosed isect_memberEquality_alt voidElimination independent_isectElimination independent_pairFormation lambdaFormation_alt callbyvalueAdd baseApply closedConclusion hypothesisEquality productElimination intEquality universeIsType addExceptionCases exceptionSqequal inrFormation_alt imageMemberEquality imageElimination inlFormation_alt callbyvalueCallbyvalue callbyvalueReduce callbyvalueExceptionCases because_Cache callbyvalueMultiply multiplyExceptionCases sqleReflexivity independent_functionElimination

Latex:
\mforall{}[P,Q:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].
    ((\mexists{}a:\{a:\mBbbR{}|  P  a\}  .  (\mexists{}b:\mBbbR{}  [((Q  b)  \mwedge{}  (a  \mleq{}  b))]))
    {}\mRightarrow{}  (\mexists{}c:\{c:\mBbbR{}|  (r0  \mleq{}  c)  \mwedge{}  (c  <  r1)\} 
              \mforall{}a:\{a:\mBbbR{}|  P  a\}  .  \mforall{}b:\{b:\mBbbR{}|  (Q  b)  \mwedge{}  (a  \mleq{}  b)\}  .
                  \mexists{}a':\{a':\mBbbR{}|  P  a'\}  .  (\mexists{}b':\{b':\mBbbR{}|  (Q  b')  \mwedge{}  (a'  \mleq{}  b')\}    [((a  \mleq{}  a')  \mwedge{}  (b'  \mleq{}  b)  \mwedge{}  ((b'  -  a')  \mleq{}  ((\000Cb  -  a)  *  c)))]))
    {}\mRightarrow{}  (\mexists{}y:\mBbbR{}.  (y  \mmember{}  closure(\mlambda{}z.(\mdownarrow{}P  z))  \mwedge{}  y  \mmember{}  closure(\mlambda{}z.(\mdownarrow{}Q  z)))))



Date html generated: 2019_10_29-AM-10_42_10
Last ObjectModification: 2019_04_05-PM-05_08_37

Theory : reals


Home Index