f:(
a bij
a). InvFuns(a;a;f;
y.least x:. f(x)=
y) B) 
(A onto B)f:(a onto b). (y.least x:. f(x)=y) 
b inj af:(a onto b), y:b. (least x:. f(x)=y) af:(a onto b), y:b. f(least x:. f(x)=y) = y| Rank | Theorem | Name |
| 5 | f:(a bij a). InvFuns(a;a;f;y.least x:. f(x)=y) | [nsub_bij_least_preimage_inverse] |
| cites the following: | ||
| 0 | B) (A onto B) | [bijtype_sub_surjtype] |
| 4 | f:(a onto b). (y.least x:. f(x)=y) b inj a | [nsub_surj_imp_a_rev_inj] |
| 3 | f:(a onto b), y:b. (least x:. f(x)=y) a | [nsub_surj_least_preimage_total] |
| 3 | f:(a onto b), y:b. f(least x:. f(x)=y) = y | [nsub_surj_least_preimage_works] |