---

Step * 1 of Lemma finite-decidable-subset


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]} )
BY
{ (RWO "-1" (-3) THENA Auto) }

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  B  :  T  {}\mrightarrow{}  \mBbbP{}
3.  finite(T)
4.  \mforall{}x:T.  Dec(\mdownarrow{}B[x])
5.  T  \msim{}  \{x:T|  B[x]\}    +  \{x:T|  \mneg{}B[x]\} 
\mvdash{}  finite(\{t:T|  B[t]\}  )


By

---

Latex:
(RWO  "-1"  (-3)  THENA  Auto)

---

Home Index