equal
deleted
inserted
replaced
52 \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y; |
52 \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y; |
53 \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y" |
53 \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y" |
54 unfolding bij_betw_def inj_on_def by blast |
54 unfolding bij_betw_def inj_on_def by blast |
55 |
55 |
56 lemma surj_fun_eq: |
56 lemma surj_fun_eq: |
57 assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x" |
57 assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 \<circ> f) x = (g2 \<circ> f) x" |
58 shows "g1 = g2" |
58 shows "g1 = g2" |
59 proof (rule ext) |
59 proof (rule ext) |
60 fix y |
60 fix y |
61 from surj_on obtain x where "x \<in> X" and "y = f x" by blast |
61 from surj_on obtain x where "x \<in> X" and "y = f x" by blast |
62 thus "g1 y = g2 y" using eq_on by simp |
62 thus "g1 y = g2 y" using eq_on by simp |