is mentioned by
![]() ![]() ![]() ![]() ![]() ![]() Thm* IsEqFun(B;e) Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [nsub_surj_imp_a_rev_inj_gen] |
![]() ![]() ![]() ![]() ![]() ![]() Thm* IsEqFun(B;e) ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [nsub_surj_least_preimage_works_gen] |
![]() ![]() ![]() ![]() ![]() ![]() Thm* IsEqFun(B;e) ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [nsub_surj_least_preimage_total_gen] |
![]() ![]() ![]() ![]() | [eq_int_is_eq_nsub] |
In prior sections: rel 1 LogicSupplement
Try larger context:
DiscrMathExt
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html