f:(
a onto
b), y:b. f(least x:. f(x)=
y) = yb;
i,j. i=j)e:(B
B
).
Thm* IsEqFun(B;e)
(a:, f:(a onto B), y:B. f(least x:. (f(x)) e y) = y)| Rank | Theorem | Name |
| 3 | f:(a onto b), y:b. f(least x:. f(x)=y) = y | [nsub_surj_least_preimage_works] |
| cites the following: | ||
| 1 | b;i,j. i=j) | [eq_int_is_eq_nsub] |
| 2 | e:(BB).
Thm* IsEqFun(B;e) (a:, f:(a onto B), y:B. f(least x:. (f(x)) e y) = y) | [nsub_surj_least_preimage_works_gen] |