equal
deleted
inserted
replaced
343 lemma (in coset) inj_on_f: |
343 lemma (in coset) inj_on_f: |
344 "[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<oplus> \<ominus>a) (H #> a)" |
344 "[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<oplus> \<ominus>a) (H #> a)" |
345 apply (rule inj_onI) |
345 apply (rule inj_onI) |
346 apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G") |
346 apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G") |
347 prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD]) |
347 prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD]) |
348 apply (rotate_tac -1) |
|
349 apply (simp add: subsetD) |
348 apply (simp add: subsetD) |
350 done |
349 done |
351 |
350 |
352 lemma (in coset) inj_on_g: |
351 lemma (in coset) inj_on_g: |
353 "[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<oplus> a) H" |
352 "[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<oplus> a) H" |