---

Step * of Lemma finite-decidable-set

∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. Dec(P[x])) ⇒ (finite-type({x:T| P[x]} ) ⇐⇒ ∃L:T List. ∀x:T. (P[x] ⇒ (x ∈ L))))
BY
{ TACTIC:((((UnivCD THENA Auto) THEN RWO "finite-set-type" 0) THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. ∃L:T List. ∀x:T. (P[x] ⇐⇒ (x ∈ L))
⊢ ∃L:T List. ∀x:T. (P[x] ⇒ (x ∈ L))

2
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. ∃L:T List. ∀x:T. (P[x] ⇒ (x ∈ L))
⊢ ∃L:T List. ∀x:T. (P[x] ⇐⇒ (x ∈ L))

---

Latex:

---

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


By

---

Latex:
TACTIC:((((UnivCD  THENA  Auto)  THEN  RWO  "finite-set-type"  0)  THENA  Auto)
                THEN  RepeatFor  2  ((D  0  THENA  Auto))
                )

---

Home Index