473 by (metis XY assms(3) assms(4) closedin_compact_space compactin_contractive compactin_imp_closedin eq openin_closedin_eq) |
473 by (metis XY assms(3) assms(4) closedin_compact_space compactin_contractive compactin_imp_closedin eq openin_closedin_eq) |
474 then show ?thesis |
474 then show ?thesis |
475 by (simp add: topology_eq) |
475 by (simp add: topology_eq) |
476 qed |
476 qed |
477 |
477 |
|
478 lemma continuous_map_imp_closed_graph: |
|
479 assumes f: "continuous_map X Y f" and Y: "Hausdorff_space Y" |
|
480 shows "closedin (prod_topology X Y) ((\<lambda>x. (x,f x)) ` topspace X)" |
|
481 unfolding closedin_def |
|
482 proof |
|
483 show "(\<lambda>x. (x, f x)) ` topspace X \<subseteq> topspace (prod_topology X Y)" |
|
484 using continuous_map_def f by fastforce |
|
485 show "openin (prod_topology X Y) (topspace (prod_topology X Y) - (\<lambda>x. (x, f x)) ` topspace X)" |
|
486 unfolding openin_prod_topology_alt |
|
487 proof (intro allI impI) |
|
488 show "\<exists>U V. openin X U \<and> openin Y V \<and> x \<in> U \<and> y \<in> V \<and> U \<times> V \<subseteq> topspace (prod_topology X Y) - (\<lambda>x. (x, f x)) ` topspace X" |
|
489 if "(x,y) \<in> topspace (prod_topology X Y) - (\<lambda>x. (x, f x)) ` topspace X" |
|
490 for x y |
|
491 proof - |
|
492 have "x \<in> topspace X" "y \<in> topspace Y" "y \<noteq> f x" |
|
493 using that by auto |
|
494 moreover have "f x \<in> topspace Y" |
|
495 by (meson \<open>x \<in> topspace X\<close> continuous_map_def f) |
|
496 ultimately obtain U V where UV: "openin Y U" "openin Y V" "f x \<in> U" "y \<in> V" "disjnt U V" |
|
497 using Y Hausdorff_space_def by metis |
|
498 show ?thesis |
|
499 proof (intro exI conjI) |
|
500 show "openin X {x \<in> topspace X. f x \<in> U}" |
|
501 using \<open>openin Y U\<close> f openin_continuous_map_preimage by blast |
|
502 show "{x \<in> topspace X. f x \<in> U} \<times> V \<subseteq> topspace (prod_topology X Y) - (\<lambda>x. (x, f x)) ` topspace X" |
|
503 using UV by (auto simp: disjnt_iff dest: openin_subset) |
|
504 qed (use UV \<open>x \<in> topspace X\<close> in auto) |
|
505 qed |
|
506 qed |
|
507 qed |
|
508 |
478 lemma continuous_imp_closed_map: |
509 lemma continuous_imp_closed_map: |
479 "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f\<rbrakk> \<Longrightarrow> closed_map X Y f" |
510 "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f\<rbrakk> \<Longrightarrow> closed_map X Y f" |
480 by (meson closed_map_def closedin_compact_space compactin_imp_closedin image_compactin) |
511 by (meson closed_map_def closedin_compact_space compactin_imp_closedin image_compactin) |
481 |
512 |
482 lemma continuous_imp_quotient_map: |
513 lemma continuous_imp_quotient_map: |
527 by (auto simp add: compactin_subtopology) |
558 by (auto simp add: compactin_subtopology) |
528 qed |
559 qed |
529 qed |
560 qed |
530 qed |
561 qed |
531 |
562 |
532 |
563 lemma closed_map_paired_continuous_map_right: |
533 lemma Hausdorff_space_euclidean: "Hausdorff_space (euclidean :: 'a::metric_space topology)" |
564 "\<lbrakk>continuous_map X Y f; Hausdorff_space Y\<rbrakk> \<Longrightarrow> closed_map X (prod_topology X Y) (\<lambda>x. (x,f x))" |
|
565 by (simp add: continuous_map_imp_closed_graph embedding_map_graph embedding_imp_closed_map) |
|
566 |
|
567 lemma closed_map_paired_continuous_map_left: |
|
568 assumes f: "continuous_map X Y f" and Y: "Hausdorff_space Y" |
|
569 shows "closed_map X (prod_topology Y X) (\<lambda>x. (f x,x))" |
|
570 proof - |
|
571 have eq: "(\<lambda>x. (f x,x)) = (\<lambda>(a,b). (b,a)) \<circ> (\<lambda>x. (x,f x))" |
|
572 by auto |
|
573 show ?thesis |
|
574 unfolding eq |
|
575 proof (rule closed_map_compose) |
|
576 show "closed_map X (prod_topology X Y) (\<lambda>x. (x, f x))" |
|
577 using Y closed_map_paired_continuous_map_right f by blast |
|
578 show "closed_map (prod_topology X Y) (prod_topology Y X) (\<lambda>(a, b). (b, a))" |
|
579 by (metis homeomorphic_map_swap homeomorphic_imp_closed_map) |
|
580 qed |
|
581 qed |
|
582 |
|
583 lemma proper_map_paired_continuous_map_right: |
|
584 "\<lbrakk>continuous_map X Y f; Hausdorff_space Y\<rbrakk> |
|
585 \<Longrightarrow> proper_map X (prod_topology X Y) (\<lambda>x. (x,f x))" |
|
586 using closed_injective_imp_proper_map closed_map_paired_continuous_map_right |
|
587 by (metis (mono_tags, lifting) Pair_inject inj_onI) |
|
588 |
|
589 lemma proper_map_paired_continuous_map_left: |
|
590 "\<lbrakk>continuous_map X Y f; Hausdorff_space Y\<rbrakk> |
|
591 \<Longrightarrow> proper_map X (prod_topology Y X) (\<lambda>x. (f x,x))" |
|
592 using closed_injective_imp_proper_map closed_map_paired_continuous_map_left |
|
593 by (metis (mono_tags, lifting) Pair_inject inj_onI) |
|
594 |
|
595 lemma Hausdorff_space_euclidean [simp]: "Hausdorff_space (euclidean :: 'a::metric_space topology)" |
534 proof - |
596 proof - |
535 have "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V" |
597 have "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V" |
536 if "x \<noteq> y" |
598 if "x \<noteq> y" |
537 for x y :: 'a |
599 for x y :: 'a |
538 proof (intro exI conjI) |
600 proof (intro exI conjI) |