equal
deleted
inserted
replaced
30 assumes LEFT: "\<forall>a \<in> A. f'(f a) = a" and |
30 assumes LEFT: "\<forall>a \<in> A. f'(f a) = a" and |
31 RIGHT: "\<forall>a' \<in> A'. f(f' a') = a'" and |
31 RIGHT: "\<forall>a' \<in> A'. f(f' a') = a'" and |
32 IM1: "f ` A \<le> A'" and IM2: "f' ` A' \<le> A" |
32 IM1: "f ` A \<le> A'" and IM2: "f' ` A' \<le> A" |
33 shows "bij_betw f A A'" |
33 shows "bij_betw f A A'" |
34 using assms |
34 using assms |
35 proof(unfold bij_betw_def inj_on_def, auto) |
35 proof(unfold bij_betw_def inj_on_def, safe) |
36 fix a b assume *: "a \<in> A" "b \<in> A" and **: "f a = f b" |
36 fix a b assume *: "a \<in> A" "b \<in> A" and **: "f a = f b" |
37 have "a = f'(f a) \<and> b = f'(f b)" using * LEFT by simp |
37 have "a = f'(f a) \<and> b = f'(f b)" using * LEFT by simp |
38 with ** show "a = b" by simp |
38 with ** show "a = b" by simp |
39 next |
39 next |
40 fix a' assume *: "a' \<in> A'" |
40 fix a' assume *: "a' \<in> A'" |