a1,a2:A. f(a1) = f(a2) 
B 
a1 = a2A,B:Type, f:(A
B). Inj(A; B; f) Prop| Who Cites inject? | |
| 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: | Inj(A; B; f) | has structure: | inject(A; B; f) |
About:
 |  |  |  |  |  |  |  |  |