Thm*
Thm* (
x:A. B(x) 
B'(f(x))) ({x:A| B(x) } ~ {x:A'| B'(x) })f:(A
B). Bij(A; B; f) (
g:(BA). InvFuns(A;B;f;g))| Theorem | Name |
Thm*
Thm* ( x:A. B(x) B'(f(x))) ({x:A| B(x) } ~ {x:A'| B'(x) }) | [card_settype] |
| cites the following: | |
| f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A;B;f;g)) | [bij_imp_exists_inv2] |