Nuprl Lemma : decidable__exists-unit-ball-approx

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 :  all: x:A. B[x] uall: [x:A]. B[x] implies:  Q member: t ∈ T subtype_rel: A ⊆B so_apply: x[s] prop: exists: x:A. B[x]
Lemmas referenced :  unit-ball-ex-decider_wf decidable_wf unit-ball-approx_wf istype-nat
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt isect_memberFormation_alt rename introduction applyEquality cut extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis sqequalRule lambdaEquality_alt isectElimination equalityTransitivity equalitySymmetry isectIsType because_Cache functionIsType universeIsType productEquality universeEquality inhabitedIsType

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_32
Last ObjectModification: 2019_07_30-AM-11_37_35

Theory : real!vectors


Home Index