---

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


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]))
⊢ ∃L:T List. ∀x:T. (P[x] ⇒ (x ∈ L))
BY
{ Assert ⌜∀i:ℕ||L||. ∃L1:T List. ∀x:T. (L[i][x] ⇒ (x ∈ L1))⌝⋅ }

1
.....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))

2
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]))
8. ∀i:ℕ||L||. ∃L1:T List. ∀x:T. (L[i][x] ⇒ (x ∈ L1))
⊢ ∃L:T List. ∀x:T. (P[x] ⇒ (x ∈ L))

---

Latex:

---

Latex:

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{}  \mexists{}L:T  List.  \mforall{}x:T.  (P[x]  {}\mRightarrow{}  (x  \mmember{}  L))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}i:\mBbbN{}||L||.  \mexists{}L1:T  List.  \mforall{}x:T.  (L[i][x]  {}\mRightarrow{}  (x  \mmember{}  L1))\mkleeneclose{}\mcdot{}

---

Home Index