---

Step * of 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])))
BY
{ (Intros
   THEN (Subst' unit-ball-ex-decider(k;n) ~ TERMOF{decidable__exists-unit-ball-approx-1-ext:o, \\v:l, i:l} k n 0
         THENA Computation
         )
   THEN Auto) }

---

Latex:

---

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])))


By

---

Latex:
(Intros
  THEN  (Subst'  unit-ball-ex-decider(k;n)  \msim{}  TERMOF\{decidable\_\_exists-unit-ball-approx-1-ext:o,
                                                                                                  \mbackslash{}\mbackslash{}v:l,
                                                                                                  i:l\} 
                                                                                    k 
                                                                                    n  0
              THENA  Computation
              )
  THEN  Auto)

---

Home Index