---

Step * of Lemma finite-set-type-cases

∀[T:Type]
  ∀L:(T ⟶ ℙ) List
    ∀[P:T ⟶ ℙ]
      ((∀x:T. Dec(P[x]))
      ⇒ (∀Q∈L.∀x:T. Dec(Q[x]))
      ⇒ (∀Q∈L.finite-type({x:T| Q[x]} ))
      ⇒ (∀x:T. (P[x] ⇒ (∃Q∈L. Q[x])))
      ⇒ finite-type({x:T| P[x]} ))
BY
{ xxx(Auto THEN RWO "finite-decidable-set" 0 THEN Auto)xxx }

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

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:(T  {}\mrightarrow{}  \mBbbP{})  List
        \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}]
            ((\mforall{}x:T.  Dec(P[x]))
            {}\mRightarrow{}  (\mforall{}Q\mmember{}L.\mforall{}x:T.  Dec(Q[x]))
            {}\mRightarrow{}  (\mforall{}Q\mmember{}L.finite-type(\{x:T|  Q[x]\}  ))
            {}\mRightarrow{}  (\mforall{}x:T.  (P[x]  {}\mRightarrow{}  (\mexists{}Q\mmember{}L.  Q[x])))
            {}\mRightarrow{}  finite-type(\{x:T|  P[x]\}  ))


By

---

Latex:
xxx(Auto  THEN  RWO  "finite-decidable-set"  0  THEN  Auto)xxx

---

Home Index