f:(
a onto
b). (
y.least x:. f(x)=
y) 
b inj ab;i,j. i=j)e:(B
B
).
Thm* IsEqFun(B;e)
Thm*
Thm* (
a:, f:(a onto B). (y.least x:. (f(x)) e y) B inj a)| Rank | Theorem | Name |
| 4 | f:(a onto b). (y.least x:. f(x)=y) b inj a | [nsub_surj_imp_a_rev_inj] |
| cites the following: | ||
| 1 | b;i,j. i=j) | [eq_int_is_eq_nsub] |
| 3 | e:(BB).
Thm* IsEqFun(B;e) Thm*
Thm* ( a:, f:(a onto B). (y.least x:. (f(x)) e y) B inj a) | [nsub_surj_imp_a_rev_inj_gen] |