equal
deleted
inserted
replaced
221 |
221 |
222 lemmas M_elem_map_eq = M_elem_map [THEN someI_ex, THEN conjunct2] |
222 lemmas M_elem_map_eq = M_elem_map [THEN someI_ex, THEN conjunct2] |
223 |
223 |
224 lemma M_funcset_rcosets_H: |
224 lemma M_funcset_rcosets_H: |
225 "(\<lambda>x\<in>M. H #> (SOME g. g \<in> carrier G \<and> M1 #> g = x)) \<in> M \<rightarrow> rcosets H" |
225 "(\<lambda>x\<in>M. H #> (SOME g. g \<in> carrier G \<and> M1 #> g = x)) \<in> M \<rightarrow> rcosets H" |
226 by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup_imp_subset) |
226 by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup.subset) |
227 |
227 |
228 lemma inj_M_GmodH: "\<exists>f \<in> M \<rightarrow> rcosets H. inj_on f M" |
228 lemma inj_M_GmodH: "\<exists>f \<in> M \<rightarrow> rcosets H. inj_on f M" |
229 apply (rule bexI) |
229 apply (rule bexI) |
230 apply (rule_tac [2] M_funcset_rcosets_H) |
230 apply (rule_tac [2] M_funcset_rcosets_H) |
231 apply (rule inj_onI, simp) |
231 apply (rule inj_onI, simp) |