equal
deleted
inserted
replaced
413 group_hom group_hom.axioms(1) subgroup.mem_carrier by metis |
413 group_hom group_hom.axioms(1) subgroup.mem_carrier by metis |
414 hence inR2: "?h \<in> (stabilizer G \<phi> x) #> r2" |
414 hence inR2: "?h \<in> (stabilizer G \<phi> x) #> r2" |
415 using g2 r2 by blast |
415 using g2 r2 by blast |
416 |
416 |
417 have "R1 \<inter> R2 \<noteq> {}" using inR1 inR2 r1 r2 by blast |
417 have "R1 \<inter> R2 \<noteq> {}" using inR1 inR2 r1 r2 by blast |
418 thus ?thesis using stabilizer_subgroup group.rcos_disjoint[of G "stabilizer G \<phi> x" R1 R2] |
418 thus ?thesis |
419 assms group_hom group_hom.axioms(1) by blast |
419 using stabilizer_subgroup group.rcos_disjoint[of G "stabilizer G \<phi> x"] assms group_hom group_hom.axioms(1) |
|
420 unfolding disjnt_def pairwise_def by blast |
420 qed |
421 qed |
421 |
422 |
422 lemma (in group_action) orbit_stab_fun_is_surj: |
423 lemma (in group_action) orbit_stab_fun_is_surj: |
423 assumes "x \<in> E" "y \<in> orbit G \<phi> x" |
424 assumes "x \<in> E" "y \<in> orbit G \<phi> x" |
424 shows "\<exists>R \<in> rcosets (stabilizer G \<phi> x). \<phi> (inv (SOME h. h \<in> R)) x = y" |
425 shows "\<exists>R \<in> rcosets (stabilizer G \<phi> x). \<phi> (inv (SOME h. h \<in> R)) x = y" |