---

Step * 1 1 of Lemma finite-set-type-cases

.....assertion..... 
1. [T] : Type
2. L : (T ⟶ ℙ) List
3. [P] : T ⟶ ℙ
4. ∀x:T. Dec(P[x])
5. (∀Q∈L.∀x:T. Dec(Q[x]))
6. (∀Q∈L.finite-type({x:T| Q[x]} ))
7. ∀x:T. (P[x] ⇒ (∃Q∈L. Q[x]))
⊢ ∀i:ℕ||L||. ∃L1:T List. ∀x:T. (L[i][x] ⇒ (x ∈ L1))
BY
{ xxx(Auto THEN With ⌜i⌝ (D (-3))⋅ THEN Auto THEN (RWO "finite-decidable-set" (-1)) THEN Auto)xxx }

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  L  :  (T  {}\mrightarrow{}  \mBbbP{})  List
3.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x:T.  Dec(P[x])
5.  (\mforall{}Q\mmember{}L.\mforall{}x:T.  Dec(Q[x]))
6.  (\mforall{}Q\mmember{}L.finite-type(\{x:T|  Q[x]\}  ))
7.  \mforall{}x:T.  (P[x]  {}\mRightarrow{}  (\mexists{}Q\mmember{}L.  Q[x]))
\mvdash{}  \mforall{}i:\mBbbN{}||L||.  \mexists{}L1:T  List.  \mforall{}x:T.  (L[i][x]  {}\mRightarrow{}  (x  \mmember{}  L1))


By

---

Latex:
xxx(Auto  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  (-3))\mcdot{}  THEN  Auto  THEN  (RWO  "finite-decidable-set"  (-1))  THEN  Auto)xxx

---

Home Index