|T| == 
f:(S
T). Surj(S; T; f)
Thm* 
S,T:Type. |S| |T| 
Prop
b:B. a:A. f(a) = b
Thm* A,B:Type, f:(AB). Surj(A; B; f) Prop
| card_ge |
Def |S| |T| == f:(ST). Surj(S; T; f)
Thm* |
| surject |
Def Surj(A; B; f) == b:B. a:A. f(a) = b
Thm* |
About:
 |  |  |  |  |
 |  |  |  |