A,B:Type, f:(A
B). Bij(A; B; f) 
PropA,B,C:Type, f:(BC), g:(AB). f o g ACa1,a2:A. f(a1) = f(a2) B 
a1 = a2A,B:Type, f:(AB). Inj(A; B; f) Propb:B. 
a:A. f(a) = bA,B:Type, f:(AB). Surj(A; B; f) Prop| Some definitions of interest. | |
| biject | Def Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f) |
| Thm* A,B:Type, f:(AB). Bij(A; B; f) Prop | |
| compose | Def (f o g)(x) == f(g(x)) |
| Thm* A,B,C:Type, f:(BC), g:(AB). f o g AC | |
| inject | Def Inj(A; B; f) == a1,a2:A. f(a1) = f(a2) B a1 = a2 |
| Thm* A,B:Type, f:(AB). Inj(A; B; f) Prop | |
| surject | Def Surj(A; B; f) == b:B. a:A. f(a) = b |
| Thm* A,B:Type, f:(AB). Surj(A; B; f) Prop |
About:
 |  |  |  |  |  |
 |  |  |  |
 |