Nuprl Lemma : unit-ball-ex-decider_wf

k,n:ℕ.
  (unit-ball-ex-decider(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-ex-decider: unit-ball-ex-decider(k;n) 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 member: t ∈ T function: x:A ⟶ B[x]
Definitions unfolded in proof :  all: x:A. B[x] unit-ball-ex-decider: unit-ball-ex-decider(k;n) primrec: primrec(n;b;c) primtailrec: primtailrec(n;i;b;f) decidable__exists-unit-ball-approx-1-ext member: t ∈ T subtype_rel: A ⊆B uall: [x:A]. B[x] prop: implies:  Q so_apply: x[s] exists: x:A. B[x]
Lemmas referenced :  decidable__exists-unit-ball-approx-1-ext subtype_rel_self nat_wf unit-ball-approx_wf decidable_wf istype-nat
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt sqequalRule applyEquality cut thin instantiate extract_by_obid hypothesis introduction sqequalHypSubstitution isectElimination functionEquality cumulativity isectEquality hypothesisEquality universeEquality productEquality inhabitedIsType

Latex:
\mforall{}k,n:\mBbbN{}.
    (unit-ball-ex-decider(k;n)  \mmember{}  \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_30
Last ObjectModification: 2019_07_30-AM-11_35_40

Theory : real!vectors


Home Index