---

Step * 1 1 of Lemma int_enumerability_nat


1. T : Type@i'
2. f :   T@i
3. Surj(;T;f)@i
 Surj(;T;z.if z <z 0 then f (((-2) * z) - 1) else f (2 * z) fi )
BY
{ (Unfold `surject` 0 THEN Unfold `surject` (-1) THEN (D 0 THENA Auto)) }

1
1. T : Type@i'
2. f :   T@i
3. b:T. a:. ((f a) = b)@i
4. b : T@i
 a:. (((z.if z <z 0 then f (((-2) * z) - 1) else f (2 * z) fi ) a) = b)



1.  T  :  Type@i'
2.  f  :  \mBbbN{}  {}\mrightarrow{}  T@i
3.  Surj(\mBbbN{};T;f)@i
\mvdash{}  Surj(\mBbbZ{};T;\mlambda{}z.if  z  <z  0  then  f  (((-2)  *  z)  -  1)  else  f  (2  *  z)  fi  )


By

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



Home Index