e:(B
B
).
Thm* IsEqFun(B;e)
(a:
, f:(a onto
B), y:B. f(least x:. (f(x)) e y) = y)k:, p:{p:(k)| 
i:k. p(i) }. p(least i:. p(i))k:, p:{p:(k)| i:k. p(i) }. (least i:. p(i)) 
k| Rank | Theorem | Name |
| 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] |
| cites the following: | ||
| 1 | k:, p:{p:(k)| i:k. p(i) }. p(least i:. p(i)) | [least_satisfies] |
| 1 | k:, p:{p:(k)| i:k. p(i) }. (least i:. p(i)) k | [least_wf] |