259 thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast |
259 thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast |
260 qed |
260 qed |
261 ultimately show "finite (UNIV :: 'a set)" by simp |
261 ultimately show "finite (UNIV :: 'a set)" by simp |
262 qed |
262 qed |
263 |
263 |
|
264 lemma image_inv_into_cancel: |
|
265 assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'" |
|
266 shows "f `((inv_into A f)`B') = B'" |
|
267 using assms |
|
268 proof (auto simp add: f_inv_into_f) |
|
269 let ?f' = "(inv_into A f)" |
|
270 fix a' assume *: "a' \<in> B'" |
|
271 then have "a' \<in> A'" using SUB by auto |
|
272 then have "a' = f (?f' a')" |
|
273 using SURJ by (auto simp add: f_inv_into_f) |
|
274 then show "a' \<in> f ` (?f' ` B')" using * by blast |
|
275 qed |
|
276 |
|
277 lemma inv_into_inv_into_eq: |
|
278 assumes "bij_betw f A A'" "a \<in> A" |
|
279 shows "inv_into A' (inv_into A f) a = f a" |
|
280 proof - |
|
281 let ?f' = "inv_into A f" let ?f'' = "inv_into A' ?f'" |
|
282 have 1: "bij_betw ?f' A' A" using assms |
|
283 by (auto simp add: bij_betw_inv_into) |
|
284 obtain a' where 2: "a' \<in> A'" and 3: "?f' a' = a" |
|
285 using 1 `a \<in> A` unfolding bij_betw_def by force |
|
286 hence "?f'' a = a'" |
|
287 using `a \<in> A` 1 3 by (auto simp add: f_inv_into_f bij_betw_def) |
|
288 moreover have "f a = a'" using assms 2 3 |
|
289 by (auto simp add: inv_into_f_f bij_betw_def) |
|
290 ultimately show "?f'' a = f a" by simp |
|
291 qed |
|
292 |
|
293 lemma inj_on_iff_surj: |
|
294 assumes "A \<noteq> {}" |
|
295 shows "(\<exists>f. inj_on f A \<and> f ` A \<le> A') \<longleftrightarrow> (\<exists>g. g ` A' = A)" |
|
296 proof safe |
|
297 fix f assume INJ: "inj_on f A" and INCL: "f ` A \<le> A'" |
|
298 let ?phi = "\<lambda>a' a. a \<in> A \<and> f a = a'" let ?csi = "\<lambda>a. a \<in> A" |
|
299 let ?g = "\<lambda>a'. if a' \<in> f ` A then (SOME a. ?phi a' a) else (SOME a. ?csi a)" |
|
300 have "?g ` A' = A" |
|
301 proof |
|
302 show "?g ` A' \<le> A" |
|
303 proof clarify |
|
304 fix a' assume *: "a' \<in> A'" |
|
305 show "?g a' \<in> A" |
|
306 proof cases |
|
307 assume Case1: "a' \<in> f ` A" |
|
308 then obtain a where "?phi a' a" by blast |
|
309 hence "?phi a' (SOME a. ?phi a' a)" using someI[of "?phi a'" a] by blast |
|
310 with Case1 show ?thesis by auto |
|
311 next |
|
312 assume Case2: "a' \<notin> f ` A" |
|
313 hence "?csi (SOME a. ?csi a)" using assms someI_ex[of ?csi] by blast |
|
314 with Case2 show ?thesis by auto |
|
315 qed |
|
316 qed |
|
317 next |
|
318 show "A \<le> ?g ` A'" |
|
319 proof- |
|
320 {fix a assume *: "a \<in> A" |
|
321 let ?b = "SOME aa. ?phi (f a) aa" |
|
322 have "?phi (f a) a" using * by auto |
|
323 hence 1: "?phi (f a) ?b" using someI[of "?phi(f a)" a] by blast |
|
324 hence "?g(f a) = ?b" using * by auto |
|
325 moreover have "a = ?b" using 1 INJ * by (auto simp add: inj_on_def) |
|
326 ultimately have "?g(f a) = a" by simp |
|
327 with INCL * have "?g(f a) = a \<and> f a \<in> A'" by auto |
|
328 } |
|
329 thus ?thesis by force |
|
330 qed |
|
331 qed |
|
332 thus "\<exists>g. g ` A' = A" by blast |
|
333 next |
|
334 fix g let ?f = "inv_into A' g" |
|
335 have "inj_on ?f (g ` A')" |
|
336 by (auto simp add: inj_on_inv_into) |
|
337 moreover |
|
338 {fix a' assume *: "a' \<in> A'" |
|
339 let ?phi = "\<lambda> b'. b' \<in> A' \<and> g b' = g a'" |
|
340 have "?phi a'" using * by auto |
|
341 hence "?phi(SOME b'. ?phi b')" using someI[of ?phi] by blast |
|
342 hence "?f(g a') \<in> A'" unfolding inv_into_def by auto |
|
343 } |
|
344 ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'" by auto |
|
345 qed |
|
346 |
|
347 lemma Ex_inj_on_UNION_Sigma: |
|
348 "\<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))" |
|
349 proof |
|
350 let ?phi = "\<lambda> a i. i \<in> I \<and> a \<in> A i" |
|
351 let ?sm = "\<lambda> a. SOME i. ?phi a i" |
|
352 let ?f = "\<lambda>a. (?sm a, a)" |
|
353 have "inj_on ?f (\<Union> i \<in> I. A i)" unfolding inj_on_def by auto |
|
354 moreover |
|
355 { { fix i a assume "i \<in> I" and "a \<in> A i" |
|
356 hence "?sm a \<in> I \<and> a \<in> A(?sm a)" using someI[of "?phi a" i] by auto |
|
357 } |
|
358 hence "?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto |
|
359 } |
|
360 ultimately |
|
361 show "inj_on ?f (\<Union> i \<in> I. A i) \<and> ?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)" |
|
362 by auto |
|
363 qed |
|
364 |
|
365 subsection {* The Cantor-Bernstein Theorem *} |
|
366 |
|
367 lemma Cantor_Bernstein_aux: |
|
368 shows "\<exists>A' h. A' \<le> A \<and> |
|
369 (\<forall>a \<in> A'. a \<notin> g`(B - f ` A')) \<and> |
|
370 (\<forall>a \<in> A'. h a = f a) \<and> |
|
371 (\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a))" |
|
372 proof- |
|
373 obtain H where H_def: "H = (\<lambda> A'. A - (g`(B - (f ` A'))))" by blast |
|
374 have 0: "mono H" unfolding mono_def H_def by blast |
|
375 then obtain A' where 1: "H A' = A'" using lfp_unfold by blast |
|
376 hence 2: "A' = A - (g`(B - (f ` A')))" unfolding H_def by simp |
|
377 hence 3: "A' \<le> A" by blast |
|
378 have 4: "\<forall>a \<in> A'. a \<notin> g`(B - f ` A')" |
|
379 using 2 by blast |
|
380 have 5: "\<forall>a \<in> A - A'. \<exists>b \<in> B - (f ` A'). a = g b" |
|
381 using 2 by blast |
|
382 (* *) |
|
383 obtain h where h_def: |
|
384 "h = (\<lambda> a. if a \<in> A' then f a else (SOME b. b \<in> B - (f ` A') \<and> a = g b))" by blast |
|
385 hence "\<forall>a \<in> A'. h a = f a" by auto |
|
386 moreover |
|
387 have "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a)" |
|
388 proof |
|
389 fix a assume *: "a \<in> A - A'" |
|
390 let ?phi = "\<lambda> b. b \<in> B - (f ` A') \<and> a = g b" |
|
391 have "h a = (SOME b. ?phi b)" using h_def * by auto |
|
392 moreover have "\<exists>b. ?phi b" using 5 * by auto |
|
393 ultimately show "?phi (h a)" using someI_ex[of ?phi] by auto |
|
394 qed |
|
395 ultimately show ?thesis using 3 4 by blast |
|
396 qed |
|
397 |
|
398 theorem Cantor_Bernstein: |
|
399 assumes INJ1: "inj_on f A" and SUB1: "f ` A \<le> B" and |
|
400 INJ2: "inj_on g B" and SUB2: "g ` B \<le> A" |
|
401 shows "\<exists>h. bij_betw h A B" |
|
402 proof- |
|
403 obtain A' and h where 0: "A' \<le> A" and |
|
404 1: "\<forall>a \<in> A'. a \<notin> g`(B - f ` A')" and |
|
405 2: "\<forall>a \<in> A'. h a = f a" and |
|
406 3: "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a)" |
|
407 using Cantor_Bernstein_aux[of A g B f] by blast |
|
408 have "inj_on h A" |
|
409 proof (intro inj_onI) |
|
410 fix a1 a2 |
|
411 assume 4: "a1 \<in> A" and 5: "a2 \<in> A" and 6: "h a1 = h a2" |
|
412 show "a1 = a2" |
|
413 proof(cases "a1 \<in> A'") |
|
414 assume Case1: "a1 \<in> A'" |
|
415 show ?thesis |
|
416 proof(cases "a2 \<in> A'") |
|
417 assume Case11: "a2 \<in> A'" |
|
418 hence "f a1 = f a2" using Case1 2 6 by auto |
|
419 thus ?thesis using INJ1 Case1 Case11 0 |
|
420 unfolding inj_on_def by blast |
|
421 next |
|
422 assume Case12: "a2 \<notin> A'" |
|
423 hence False using 3 5 2 6 Case1 by force |
|
424 thus ?thesis by simp |
|
425 qed |
|
426 next |
|
427 assume Case2: "a1 \<notin> A'" |
|
428 show ?thesis |
|
429 proof(cases "a2 \<in> A'") |
|
430 assume Case21: "a2 \<in> A'" |
|
431 hence False using 3 4 2 6 Case2 by auto |
|
432 thus ?thesis by simp |
|
433 next |
|
434 assume Case22: "a2 \<notin> A'" |
|
435 hence "a1 = g(h a1) \<and> a2 = g(h a2)" using Case2 4 5 3 by auto |
|
436 thus ?thesis using 6 by simp |
|
437 qed |
|
438 qed |
|
439 qed |
|
440 (* *) |
|
441 moreover |
|
442 have "h ` A = B" |
|
443 proof safe |
|
444 fix a assume "a \<in> A" |
|
445 thus "h a \<in> B" using SUB1 2 3 by (case_tac "a \<in> A'", auto) |
|
446 next |
|
447 fix b assume *: "b \<in> B" |
|
448 show "b \<in> h ` A" |
|
449 proof(cases "b \<in> f ` A'") |
|
450 assume Case1: "b \<in> f ` A'" |
|
451 then obtain a where "a \<in> A' \<and> b = f a" by blast |
|
452 thus ?thesis using 2 0 by force |
|
453 next |
|
454 assume Case2: "b \<notin> f ` A'" |
|
455 hence "g b \<notin> A'" using 1 * by auto |
|
456 hence 4: "g b \<in> A - A'" using * SUB2 by auto |
|
457 hence "h(g b) \<in> B \<and> g(h(g b)) = g b" |
|
458 using 3 by auto |
|
459 hence "h(g b) = b" using * INJ2 unfolding inj_on_def by auto |
|
460 thus ?thesis using 4 by force |
|
461 qed |
|
462 qed |
|
463 (* *) |
|
464 ultimately show ?thesis unfolding bij_betw_def by auto |
|
465 qed |
264 |
466 |
265 subsection {*Other Consequences of Hilbert's Epsilon*} |
467 subsection {*Other Consequences of Hilbert's Epsilon*} |
266 |
468 |
267 text {*Hilbert's Epsilon and the @{term split} Operator*} |
469 text {*Hilbert's Epsilon and the @{term split} Operator*} |
268 |
470 |