---

Step * 1 of Lemma finite-type-implies-finite


1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. finite-type(T)@i
4. n : ℕ
5. ℕn ~ T
6. finite-type(T)
⊢ finite(T)
BY
{ ((InstLemma `finite_functionality_wrt_equipollent` [⌜ℕn⌝;⌜T⌝]⋅ THENA Auto) THEN BHyp -1 ) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. finite-type(T)@i
4. n : ℕ
5. ℕn ~ T
6. finite-type(T)
7. finite(ℕn) ⇐⇒ finite(T)
⊢ finite(ℕn)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)@i
3.  finite-type(T)@i
4.  n  :  \mBbbN{}
5.  \mBbbN{}n  \msim{}  T
6.  finite-type(T)
\mvdash{}  finite(T)


By

---

Latex:
((InstLemma  `finite\_functionality\_wrt\_equipollent`  [\mkleeneopen{}\mBbbN{}n\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  BHyp  -1  )

---

Home Index