---

Step * of Lemma decidable-exists-finite-type

∀[T:Type]. (finite-type(T) ⇒ (∀[P:T ⟶ ℙ]. ((∀t:T. Dec(P[t])) ⇒ Dec(∃t:T. P[t]))))
BY
{ (Auto THEN D 2 THEN ExRepD THEN Decide ∃i:ℕn. P[f i] THEN Auto) }

1
.....decidable?..... 
1. [T] : Type
2. n : ℕ@i
3. f : ℕn ⟶ T@i
4. Surj(ℕn;T;f)@i
5. [P] : T ⟶ ℙ
6. ∀t:T. Dec(P[t])@i
7. ∃i:ℕn. P[f i]
⊢ Dec(∃t:T. P[t])

2
.....decidable?..... 
1. [T] : Type
2. n : ℕ@i
3. f : ℕn ⟶ T@i
4. Surj(ℕn;T;f)@i
5. [P] : T ⟶ ℙ
6. ∀t:T. Dec(P[t])@i
7. ¬(∃i:ℕn. P[f i])
⊢ Dec(∃t:T. P[t])

---

Latex:

---

Latex:
\mforall{}[T:Type].  (finite-type(T)  {}\mRightarrow{}  (\mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}t:T.  Dec(P[t]))  {}\mRightarrow{}  Dec(\mexists{}t:T.  P[t]))))


By

---

Latex:
(Auto  THEN  D  2  THEN  ExRepD  THEN  Decide  \mexists{}i:\mBbbN{}n.  P[f  i]  THEN  Auto)

---

Home Index