Nuprl Lemma : decidable__exists-unit-ball-approx-1-ext

k,n:ℕ.  ∀[P:unit-ball-approx(n;k) ⟶ ℙ]. ((∀p:unit-ball-approx(n;k). Dec(P[p]))  Dec(∃p:unit-ball-approx(n;k). P[p]))


Proof




Definitions occuring in Statement :  unit-ball-approx: unit-ball-approx(n;k) nat: decidable: Dec(P) uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] implies:  Q function: x:A ⟶ B[x]
Definitions unfolded in proof :  member: t ∈ T it: subtract: m extend-approx-ball: extend-approx-ball(n;p;z) ifthenelse: if then else fi  lt_int: i <j btrue: tt bfalse: ff int_seg_decide: int_seg_decide(d;i;j) genrec-ap: genrec-ap spreadn: spread4 decidable__exists-unit-ball-approx-1 unit-ball-approx0 decidable__exists_int_seg decidable__cand decidable__le decidable__and2 decidable__and decidable__not decidable__less_than' decidable__implies decidable__false any: any x 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] so_lambda: λ2x.t[x] top: Top so_apply: x[s] uimplies: supposing a
Lemmas referenced :  decidable__exists-unit-ball-approx-1 lifting-strict-decide istype-void strict4-decide lifting-strict-less unit-ball-approx0 decidable__exists_int_seg decidable__cand decidable__le decidable__and2 decidable__and decidable__not decidable__less_than' decidable__implies decidable__false
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

Latex:
\mforall{}k,n:\mBbbN{}.
    \mforall{}[P:unit-ball-approx(n;k)  {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}p:unit-ball-approx(n;k).  Dec(P[p]))  {}\mRightarrow{}  Dec(\mexists{}p:unit-ball-approx(n;k).  P[p]))



Date html generated: 2019_10_30-AM-11_28_24
Last ObjectModification: 2019_07_30-AM-11_34_07

Theory : real!vectors


Home Index