Step
*
1
1
2
of Lemma
decidable-exists-finite
1. [T] : Type
2. [P] : T ─→ ℙ
3. ∀x:T. Dec(P[x])@i
4. n : ℕ@i
5. f : ℕn ─→ T@i
6. ∀b:T. ∃a:ℕn. ((f a) = b ∈ T)@i
7. i : ℕn@i
8. P[f i]@i
⊢ ∃x:T. P[x]
BY
{ ((InstConcl [⌈f i⌉])⋅ THEN Auto) }
Latex:
1. [T] : Type
2. [P] : T {}\mrightarrow{} \mBbbP{}
3. \mforall{}x:T. Dec(P[x])@i
4. n : \mBbbN{}@i
5. f : \mBbbN{}n {}\mrightarrow{} T@i
6. \mforall{}b:T. \mexists{}a:\mBbbN{}n. ((f a) = b)@i
7. i : \mBbbN{}n@i
8. P[f i]@i
\mvdash{} \mexists{}x:T. P[x]
By
((InstConcl [\mkleeneopen{}f i\mkleeneclose{}])\mcdot{} THEN Auto)
Home
Index