---

Step * of Lemma int_enumerability_nat

T:Type. ((f:  T. Surj(;T;f))  (g:  T. Surj(;T;g)))
BY
{ Auto }

1
1. T : Type@i'
2. f:  T. Surj(;T;f)@i
 g:  T. Surj(;T;g)


\mforall{}T:Type.  ((\mexists{}f:\mBbbN{}  {}\mrightarrow{}  T.  Surj(\mBbbN{};T;f))  {}\mRightarrow{}  (\mexists{}g:\mBbbZ{}  {}\mrightarrow{}  T.  Surj(\mBbbZ{};T;g)))


By

Auto



Home Index