---

Step * of Lemma finite-type-equipollent

∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (finite-type(T) ⇐⇒ ∃n:ℕ. ℕn ~ T))
BY
{ (Unfolds ``finite-type equipollent`` 0 THEN Auto THEN ExRepD) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. n : ℕ
4. f : ℕn ⟶ T
5. Surj(ℕn;T;f)
⊢ ∃n:ℕ. ∃f:ℕn ⟶ T. Bij(ℕn;T;f)

---

Latex:

---

Latex:
\mforall{}[T:Type].  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (finite-type(T)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  \mBbbN{}n  \msim{}  T))


By

---

Latex:
(Unfolds  ``finite-type  equipollent``  0  THEN  Auto  THEN  ExRepD)

---

Home Index