---

Step * of Lemma decidable-exists-finite

∀[T:Type]. ∀[P:T ─→ ℙ].  ((∀x:T. Dec(P[x])) ⇒ finite-type(T) ⇒ Dec(∃x:T. P[x]))
BY
{ Auto }

1
.....decidable?..... 
1. [T] : Type
2. [P] : T ─→ ℙ
3. ∀x:T. Dec(P[x])@i
4. finite-type(T)@i
⊢ Dec(∃x:T. P[x])

---

Latex:


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


By

Auto

---

Home Index