---

Step * 1 of Lemma decidable__exists-unit-ball-approx-1

.....decidable?..... 
1. k : ℕ
2. [P] : unit-ball-approx(0;k) ⟶ ℙ
3. ∀p:unit-ball-approx(0;k). Dec(P[p])
⊢ Dec(∃p:unit-ball-approx(0;k). P[p])
BY
{ ((InstLemma `unit-ball-approx0` [⌜k⌝]⋅ THENA Auto) THEN D -1 THEN (D 3 With ⌜⋅⌝  THENA (SubsumeC ⌜Top⌝⋅ THEN Auto))) }

1
1. k : ℕ
2. [P] : unit-ball-approx(0;k) ⟶ ℙ
3. unit-ball-approx(0;k) ⊆r Top
4. Top ⊆r unit-ball-approx(0;k)
5. Dec(P[⋅])
⊢ Dec(∃p:unit-ball-approx(0;k). P[p])

---

Latex:

---

Latex:
.....decidable?..... 
1.  k  :  \mBbbN{}
2.  [P]  :  unit-ball-approx(0;k)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}p:unit-ball-approx(0;k).  Dec(P[p])
\mvdash{}  Dec(\mexists{}p:unit-ball-approx(0;k).  P[p])


By

---

Latex:
((InstLemma  `unit-ball-approx0`  [\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (D  3  With  \mkleeneopen{}\mcdot{}\mkleeneclose{}    THENA  (SubsumeC  \mkleeneopen{}Top\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index