406 } |
406 } |
407 ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'" by auto |
407 ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'" by auto |
408 qed |
408 qed |
409 |
409 |
410 lemma Ex_inj_on_UNION_Sigma: |
410 lemma Ex_inj_on_UNION_Sigma: |
411 "\<exists>f. (inj_on f (\<Union> i \<in> I. A i) \<and> f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i))" |
411 "\<exists>f. (inj_on f (\<Union>i \<in> I. A i) \<and> f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i))" |
412 proof |
412 proof |
413 let ?phi = "\<lambda> a i. i \<in> I \<and> a \<in> A i" |
413 let ?phi = "\<lambda> a i. i \<in> I \<and> a \<in> A i" |
414 let ?sm = "\<lambda> a. SOME i. ?phi a i" |
414 let ?sm = "\<lambda> a. SOME i. ?phi a i" |
415 let ?f = "\<lambda>a. (?sm a, a)" |
415 let ?f = "\<lambda>a. (?sm a, a)" |
416 have "inj_on ?f (\<Union> i \<in> I. A i)" unfolding inj_on_def by auto |
416 have "inj_on ?f (\<Union>i \<in> I. A i)" unfolding inj_on_def by auto |
417 moreover |
417 moreover |
418 { { fix i a assume "i \<in> I" and "a \<in> A i" |
418 { { fix i a assume "i \<in> I" and "a \<in> A i" |
419 hence "?sm a \<in> I \<and> a \<in> A(?sm a)" using someI[of "?phi a" i] by auto |
419 hence "?sm a \<in> I \<and> a \<in> A(?sm a)" using someI[of "?phi a" i] by auto |
420 } |
420 } |
421 hence "?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto |
421 hence "?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto |
422 } |
422 } |
423 ultimately |
423 ultimately |
424 show "inj_on ?f (\<Union> i \<in> I. A i) \<and> ?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)" |
424 show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)" |
425 by auto |
425 by auto |
426 qed |
426 qed |
427 |
427 |
428 lemma inv_unique_comp: |
428 lemma inv_unique_comp: |
429 assumes fg: "f \<circ> g = id" |
429 assumes fg: "f \<circ> g = id" |