---

Step * of Lemma decidable__all-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
{ ((D 0 THENA Auto) THEN InductionOnNat THEN Auto) }

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

2
.....decidable?..... 
1. k : ℕ
2. n : ℤ
3. [%1] : 0 < n
4. ∀[P:unit-ball-approx(n - 1;k) ⟶ ℙ]
     ((∀p:unit-ball-approx(n - 1;k). Dec(P[p])) ⇒ Dec(∀p:unit-ball-approx(n - 1;k). P[p]))
5. [P] : unit-ball-approx(n;k) ⟶ ℙ
6. ∀p:unit-ball-approx(n;k). Dec(P[p])
⊢ Dec(∀p:unit-ball-approx(n;k). P[p])

---

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(\mforall{}p:unit-ball-approx(n;k).  P[p]))


By

---

Latex:
((D  0  THENA  Auto)  THEN  InductionOnNat  THEN  Auto)

---

Home Index