---

Step * 1 1 of Lemma finite-type-equipollent


1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. f : ℕ0 ⟶ T
4. Surj(ℕ0;T;f)
⊢ ∃n:ℕ. ∃f:ℕn ⟶ T. Bij(ℕn;T;f)
BY
{ ((InstConcl [⌜0⌝;⌜f⌝]⋅ THEN Auto) THEN RepeatFor 2 ((D 0 THEN Auto))) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  f  :  \mBbbN{}0  {}\mrightarrow{}  T
4.  Surj(\mBbbN{}0;T;f)
\mvdash{}  \mexists{}n:\mBbbN{}.  \mexists{}f:\mBbbN{}n  {}\mrightarrow{}  T.  Bij(\mBbbN{}n;T;f)


By

---

Latex:
((InstConcl  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index