---

Step * of Lemma finite-decidable-subset

∀T:Type. ∀B:T ⟶ ℙ.  (finite(T) ⇒ (∀x:T. Dec(↓B[x])) ⇒ finite({t:T| B[t]} ))
BY
{ (Auto THEN (InstLemma `equipollent-split` [⌜T⌝;⌜B⌝]⋅ THENA Auto)) }

1
1. T : Type
2. B : T ⟶ ℙ
3. finite(T)
4. ∀x:T. Dec(↓B[x])
5. T ~ {x:T| B[x]}  + {x:T| ¬B[x]} 
⊢ finite({t:T| B[t]} )

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}B:T  {}\mrightarrow{}  \mBbbP{}.    (finite(T)  {}\mRightarrow{}  (\mforall{}x:T.  Dec(\mdownarrow{}B[x]))  {}\mRightarrow{}  finite(\{t:T|  B[t]\}  ))


By

---

Latex:
(Auto  THEN  (InstLemma  `equipollent-split`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index