---

Step * of Lemma not_total_enumerable_inc

(f:    . Surj(;  ;f))
BY
{ (((D 0 THEN Auto) THEN D (-1)) THEN Unfold `surject` (-1)) }

1
1. f :     @i
2. b:  . a:. ((f a) = b)@i
 False


\mneg{}(\mexists{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbB{}.  Surj(\mBbbZ{};\mBbbZ{}  {}\mrightarrow{}  \mBbbB{};f))


By

(((D  0  THEN  Auto)  THEN  D  (-1))  THEN  Unfold  `surject`  (-1))



Home Index