---

Step * 1 1 of Lemma finite-decidable-subset


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]} )
BY
{ (RWO "finite-union<" (-3) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  B  :  T  {}\mrightarrow{}  \mBbbP{}
3.  finite(\{x:T|  B[x]\}    +  \{x:T|  \mneg{}B[x]\}  )
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  "finite-union<"  (-3)  THEN  Auto)

---

Home Index