---

Step * 1 1 of Lemma decidable__exists-unit-ball-approx-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])
BY
{ (RepeatFor 2 (ParallelLast) THEN Try (ParallelLast)) }

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. P[⋅]
⊢ ∃p:unit-ball-approx(0;k). P[p]

2
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. ∃p:unit-ball-approx(0;k). P[p]
⊢ P[⋅]

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  [P]  :  unit-ball-approx(0;k)  {}\mrightarrow{}  \mBbbP{}
3.  unit-ball-approx(0;k)  \msubseteq{}r  Top
4.  Top  \msubseteq{}r  unit-ball-approx(0;k)
5.  Dec(P[\mcdot{}])
\mvdash{}  Dec(\mexists{}p:unit-ball-approx(0;k).  P[p])


By

---

Latex:
(RepeatFor  2  (ParallelLast)  THEN  Try  (ParallelLast))

---

Home Index