Thm* f:( a bij a). InvFuns( a; a;f; y.least x: . f(x)= y) | [nsub_bij_least_preimage_inverse] |
Thm* f:( a onto b). ( y.least x: . f(x)= y) b inj a | [nsub_surj_imp_a_rev_inj] |
Thm* e:(B![](FONT/dash.png) B![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* IsEqFun(B;e)
Thm* ![](FONT/eq.png)
Thm* ( a: , f:( a onto B). ( y.least x: . (f(x)) e y) B inj a) | [nsub_surj_imp_a_rev_inj_gen] |
Thm* f:( a onto b), y: b. f(least x: . f(x)= y) = y | [nsub_surj_least_preimage_works] |
Thm* e:(B![](FONT/dash.png) B![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* IsEqFun(B;e) ![](FONT/eq.png) ( a: , f:( a onto B), y:B. f(least x: . (f(x)) e y) = y) | [nsub_surj_least_preimage_works_gen] |
Thm* f:( a onto b), y: b. (least x: . f(x)= y) a | [nsub_surj_least_preimage_total] |
Thm* e:(B![](FONT/dash.png) B![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* IsEqFun(B;e) ![](FONT/eq.png) ( a: , f:( a onto B), y:B. (least x: . (f(x)) e y) a) | [nsub_surj_least_preimage_total_gen] |
Thm* p:{p:(![](FONT/nat.png) ![](FONT/dash.png) ![](FONT/then_med.png) )| i: . p(i) }. p(least i: . p(i)) | [least_satisfies2] |
Thm* p:{p:(![](FONT/nat.png) ![](FONT/dash.png) ![](FONT/then_med.png) )| i: . p(i) }, j: (least i: . p(i)). p(j) | [least_is_least2] |
Thm* k: , p:{p:( k![](FONT/dash.png) ![](FONT/then_med.png) )| i: k. p(i) }, j: (least i: . p(i)). p(j) | [least_is_least] |
Thm* k: , p:{p:( k![](FONT/dash.png) ![](FONT/then_med.png) )| i: k. p(i) }. p(least i: . p(i)) | [least_satisfies] |
Thm* p:{p:(![](FONT/nat.png) ![](FONT/dash.png) ![](FONT/then_med.png) )| i: . p(i) }.
Thm* (least i: . p(i)) {i: | p(i) & ( j: . j<i ![](FONT/eq.png) p(j)) } | [least_characterized2] |
Thm* k: , p:{p:( k![](FONT/dash.png) ![](FONT/then_med.png) )| i: k. p(i) }.
Thm* (least i: . p(i)) {i: k| p(i) & ( j: i. p(j)) } | [least_characterized] |