A,B:Type, f:(A
B). Bij(A; B; f) 
Propb:B. 
a:A. f(a) = bA,B:Type, f:(AB). Surj(A; B; f) Propa1,a2:A. f(a1) = f(a2) B 
a1 = a2A,B:Type, f:(AB). Inj(A; B; f) Prop| Who Cites biject? | |
| 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 | |
| surject | Def Surj(A; B; f) == b:B. a:A. f(a) = b |
| Thm* A,B:Type, f:(AB). Surj(A; B; f) Prop | |
| 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 |
| Syntax: | Bij(A; B; f) | has structure: | biject(A; B; f) |
About:
 |  |  |  |  |  |
 |  |  |  |
 |