Rank | Theorem | Name |
2 | Thm* (A ~ A')  (B ~ B')  ((A inj B) ~ (A' inj B')) | [injection_type_functionality_wrt_ooc] |
cites the following: |
1 | Thm* InvFuns(A;B;f;g)  Inj(A; B; f) & Inj(B; A; g) | [invfuns_are_inj] |
0 | Thm* Inj(A; B; g)  Inj(B; C; f)  Inj(A; C; f o g) | [comp_preserves_inj] |