equal
deleted
inserted
replaced
60 "g: Y->X ==> \ |
60 "g: Y->X ==> \ |
61 \ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \ |
61 \ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \ |
62 \ X - lfp(X, %W. X - g``(Y - f``W)) "; |
62 \ X - lfp(X, %W. X - g``(Y - f``W)) "; |
63 by (res_inst_tac [("P", "%u. ?v = X-u")] |
63 by (res_inst_tac [("P", "%u. ?v = X-u")] |
64 (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1); |
64 (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1); |
65 by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, Diff_subset, |
65 by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, |
66 gfun RS fun_is_rel RS image_subset]) 1); |
66 gfun RS fun_is_rel RS image_subset]) 1); |
67 val Banach_last_equation = result(); |
67 val Banach_last_equation = result(); |
68 |
68 |
69 val prems = goal SB_thy |
69 val prems = goal SB_thy |
70 "[| f: X->Y; g: Y->X |] ==> \ |
70 "[| f: X->Y; g: Y->X |] ==> \ |