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: P ⇒ 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 ⊆r B,
uall: ∀[x:A]. B[x],
prop: ℙ,
implies: P ⇒ 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