A,B:Type, f:(A
B). Bij(A; B; f) 
PropA,B:Type, f:(AB), g:(BA). InvFuns(A; B; f; g) 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 | |
| inv_funs | Def InvFuns(A; B; f; g) == g o f = Id & f o g = Id |
| Thm* A,B:Type, f:(AB), g:(BA). InvFuns(A; B; f; g) Prop |
About:
 |  |  |  |  |  |  |  |