A:Type.
(A Discrete) 
(k:
, f:(k
A). f 
k onto
{a:A| 
i:k. a = f(i) }) A:Type.
(A Discrete) (k:, f:(kA). f k onto {a:A| i:k. a = f(i) })| By: |
Thm* (A Discrete) Thm*
Thm* ( k:, f:(kA).
Thm* ({a:A| i:k. a = f(i) } Type
Thm* (& f k{a:A| i:k. a = f(i) }
Thm* (& Surj( k; {a:A| i:k. a = f(i) }; f))
THEN ExistHD Hyp:-1 |
| 1 |
2. A Discrete 3. k :
4. f : kA
5. {a:A| i:k. a = f(i) } Type
6. f k{a:A| i:k. a = f(i) }
7. Surj( k; {a:A| i:k. a = f(i) }; f)
f k onto {a:A| i:k. a = f(i) } | 1 step |
About:
 |  |  |  |  |
 |  |  |  |  |