equal
deleted
inserted
replaced
140 qed "subset_inj_on"; |
140 qed "subset_inj_on"; |
141 |
141 |
142 |
142 |
143 (** surj **) |
143 (** surj **) |
144 |
144 |
145 val [major] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; |
145 val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; |
146 by (blast_tac (claset() addIs [major RS sym]) 1); |
146 by (blast_tac (claset() addIs [prem RS sym]) 1); |
147 qed "surjI"; |
147 qed "surjI"; |
148 |
148 |
149 Goalw [surj_def] "surj f ==> range f = UNIV"; |
149 Goalw [surj_def] "surj f ==> range f = UNIV"; |
150 by Auto_tac; |
150 by Auto_tac; |
151 qed "surj_range"; |
151 qed "surj_range"; |
|
152 |
|
153 Goalw [surj_def] "surj f ==> EX x. y = f x"; |
|
154 by (Blast_tac 1); |
|
155 qed "surjD"; |
152 |
156 |
153 |
157 |
154 (*** Lemmas about injective functions and inv ***) |
158 (*** Lemmas about injective functions and inv ***) |
155 |
159 |
156 Goalw [o_def] "[| inj_on f A; inj_on g (range f) |] ==> inj_on (g o f) A"; |
160 Goalw [o_def] "[| inj_on f A; inj_on g (range f) |] ==> inj_on (g o f) A"; |