---

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

.....wf..... 
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)
6. P[p]
7. z : unit-ball-approx(0;k)
⊢ P[z] ∈ ℙ
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
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.  p  :  unit-ball-approx(0;k)
6.  P[p]
7.  z  :  unit-ball-approx(0;k)
\mvdash{}  P[z]  \mmember{}  \mBbbP{}


By

---

Latex:
Auto

---

Home Index