Step * of Lemma finite-type-equipollent

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

1
1. [T] Type
2. ∀x,y:T.  Dec(x y ∈ T)
3. : ℕ
4. : ℕ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