B == {f:(A
B)| Bij(A; B; f) } B == {f:(AB)| Bij(A; B; f) }is mentioned by
 a bij a) ~ (a a) | [nsub_bij_ooc_invpair] |
| k inj k) ~ (k bij k) | [nsub_inj_ooc_nsub_bij] |
| k inj k) =ext (k bij k) | [nsub_inj_exteq_nsub_bij] |
| k onto k) ~ (k bij k) | [nsub_surj_ooc_nsub_bij] |
| k onto k) =ext (k bij k) | [nsub_surj_exteq_nsub_bij] |
 f:(a bij a). InvFuns(a;a;f; y.least x:. f(x)= y) | [nsub_bij_least_preimage_inverse] |
B) ~ ((A inj B) (A onto B)) | [bijtype_ooc_inj_isect_surjtype] |
  (k:, f:(k inj A). f  k bij {a:A|  i:k. a = f(i) }) | [nsub_inj_discr_range_bijtype] |
| B) =ext ((A inj B)(A onto B)) | [bijtype_exteq_inj_isect_surjtype] |
B)  (A onto B) | [bijection_type_inc_surj] |
| B) (A onto B) | [bijtype_sub_surjtype] |
| B) (A inj B) | [bijection_type_inc_inj] |
| B) (A inj B) | [bijtype_sub_injtype] |
Try larger context:
DiscrMathExt
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html