---

Step * of 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]))
BY
{ (Intros THEN RenameVar `d' (-1) THEN UseWitness ⌜unit-ball-ex-decider(k;n) d⌝⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros  THEN  RenameVar  `d'  (-1)  THEN  UseWitness  \mkleeneopen{}unit-ball-ex-decider(k;n)  d\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index