---

Step * of Lemma finite-subtype

∀[B:Type]. ∀P:B ⟶ 𝔹. (finite-type(B) ⇒ finite-type({b:B| ↑P[b]} ))
BY
{ (((RepeatFor 2 ((D 0 THENA Auto)) THEN RWO "finite-type-iff-list" 0) THENA Auto) THEN Auto THEN ExRepD) }

1
1. [B] : Type
2. P : B ⟶ 𝔹@i
3. L : B List@i
4. ∀x:B. (x ∈ L)@i
⊢ ∃L:{b:B| ↑P[b]}  List. ∀x:{b:B| ↑P[b]} . (x ∈ L)

---

Latex:

---

Latex:
\mforall{}[B:Type].  \mforall{}P:B  {}\mrightarrow{}  \mBbbB{}.  (finite-type(B)  {}\mRightarrow{}  finite-type(\{b:B|  \muparrow{}P[b]\}  ))


By

---

Latex:
(((RepeatFor  2  ((D  0  THENA  Auto))  THEN  RWO  "finite-type-iff-list"  0)  THENA  Auto)
  THEN  Auto
  THEN  ExRepD)

---

Home Index