2424 qed (use assms in auto) |
2424 qed (use assms in auto) |
2425 then show "openin (top_of_set (f ` S)) (f ` S \<inter> g -` T)" |
2425 then show "openin (top_of_set (f ` S)) (f ` S \<inter> g -` T)" |
2426 by (simp add: eq) |
2426 by (simp add: eq) |
2427 qed |
2427 qed |
2428 |
2428 |
|
2429 lemma invariance_of_domain_homeomorphism: |
|
2430 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
2431 assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S" |
|
2432 obtains g where "homeomorphism S (f ` S) f g" |
|
2433 proof |
|
2434 show "homeomorphism S (f ` S) f (inv_into S f)" |
|
2435 by (simp add: assms continuous_on_inverse_open homeomorphism_def) |
|
2436 qed |
|
2437 |
|
2438 corollary invariance_of_domain_homeomorphic: |
|
2439 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
2440 assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S" |
|
2441 shows "S homeomorphic (f ` S)" |
|
2442 using%unimportant invariance_of_domain_homeomorphism [OF assms] |
|
2443 by%unimportant (meson homeomorphic_def) |
|
2444 |
|
2445 lemma continuous_image_subset_interior: |
|
2446 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
2447 assumes "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)" |
|
2448 shows "f ` (interior S) \<subseteq> interior(f ` S)" |
|
2449 proof (rule interior_maximal) |
|
2450 show "f ` interior S \<subseteq> f ` S" |
|
2451 by (simp add: image_mono interior_subset) |
|
2452 show "open (f ` interior S)" |
|
2453 using assms |
|
2454 by (auto simp: subset_inj_on interior_subset continuous_on_subset invariance_of_domain_gen) |
|
2455 qed |
|
2456 |
|
2457 lemma homeomorphic_interiors_same_dimension: |
|
2458 fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" |
|
2459 assumes "S homeomorphic T" and dimeq: "DIM('a) = DIM('b)" |
|
2460 shows "(interior S) homeomorphic (interior T)" |
|
2461 using assms [unfolded homeomorphic_minimal] |
|
2462 unfolding homeomorphic_def |
|
2463 proof (clarify elim!: ex_forward) |
|
2464 fix f g |
|
2465 assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y" |
|
2466 and contf: "continuous_on S f" and contg: "continuous_on T g" |
|
2467 then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T" |
|
2468 by (auto simp: inj_on_def intro: rev_image_eqI) metis+ |
|
2469 have fim: "f ` interior S \<subseteq> interior T" |
|
2470 using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp |
|
2471 have gim: "g ` interior T \<subseteq> interior S" |
|
2472 using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp |
|
2473 show "homeomorphism (interior S) (interior T) f g" |
|
2474 unfolding homeomorphism_def |
|
2475 proof (intro conjI ballI) |
|
2476 show "\<And>x. x \<in> interior S \<Longrightarrow> g (f x) = x" |
|
2477 by (meson \<open>\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x\<close> subsetD interior_subset) |
|
2478 have "interior T \<subseteq> f ` interior S" |
|
2479 proof |
|
2480 fix x assume "x \<in> interior T" |
|
2481 then have "g x \<in> interior S" |
|
2482 using gim by blast |
|
2483 then show "x \<in> f ` interior S" |
|
2484 by (metis T \<open>x \<in> interior T\<close> image_iff interior_subset subsetCE) |
|
2485 qed |
|
2486 then show "f ` interior S = interior T" |
|
2487 using fim by blast |
|
2488 show "continuous_on (interior S) f" |
|
2489 by (metis interior_subset continuous_on_subset contf) |
|
2490 show "\<And>y. y \<in> interior T \<Longrightarrow> f (g y) = y" |
|
2491 by (meson T subsetD interior_subset) |
|
2492 have "interior S \<subseteq> g ` interior T" |
|
2493 proof |
|
2494 fix x assume "x \<in> interior S" |
|
2495 then have "f x \<in> interior T" |
|
2496 using fim by blast |
|
2497 then show "x \<in> g ` interior T" |
|
2498 by (metis S \<open>x \<in> interior S\<close> image_iff interior_subset subsetCE) |
|
2499 qed |
|
2500 then show "g ` interior T = interior S" |
|
2501 using gim by blast |
|
2502 show "continuous_on (interior T) g" |
|
2503 by (metis interior_subset continuous_on_subset contg) |
|
2504 qed |
|
2505 qed |
|
2506 |
|
2507 lemma homeomorphic_open_imp_same_dimension: |
|
2508 fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" |
|
2509 assumes "S homeomorphic T" "open S" "S \<noteq> {}" "open T" "T \<noteq> {}" |
|
2510 shows "DIM('a) = DIM('b)" |
|
2511 using assms |
|
2512 apply (simp add: homeomorphic_minimal) |
|
2513 apply (rule order_antisym; metis inj_onI invariance_of_dimension) |
|
2514 done |
|
2515 |
|
2516 proposition homeomorphic_interiors: |
|
2517 fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" |
|
2518 assumes "S homeomorphic T" "interior S = {} \<longleftrightarrow> interior T = {}" |
|
2519 shows "(interior S) homeomorphic (interior T)" |
|
2520 proof (cases "interior T = {}") |
|
2521 case True |
|
2522 with assms show ?thesis by auto |
|
2523 next |
|
2524 case False |
|
2525 then have "DIM('a) = DIM('b)" |
|
2526 using assms |
|
2527 apply (simp add: homeomorphic_minimal) |
|
2528 apply (rule order_antisym; metis continuous_on_subset inj_onI inj_on_subset interior_subset invariance_of_dimension open_interior) |
|
2529 done |
|
2530 then show ?thesis |
|
2531 by (rule homeomorphic_interiors_same_dimension [OF \<open>S homeomorphic T\<close>]) |
|
2532 qed |
|
2533 |
|
2534 lemma homeomorphic_frontiers_same_dimension: |
|
2535 fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" |
|
2536 assumes "S homeomorphic T" "closed S" "closed T" and dimeq: "DIM('a) = DIM('b)" |
|
2537 shows "(frontier S) homeomorphic (frontier T)" |
|
2538 using assms [unfolded homeomorphic_minimal] |
|
2539 unfolding homeomorphic_def |
|
2540 proof (clarify elim!: ex_forward) |
|
2541 fix f g |
|
2542 assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y" |
|
2543 and contf: "continuous_on S f" and contg: "continuous_on T g" |
|
2544 then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T" |
|
2545 by (auto simp: inj_on_def intro: rev_image_eqI) metis+ |
|
2546 have "g ` interior T \<subseteq> interior S" |
|
2547 using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp |
|
2548 then have fim: "f ` frontier S \<subseteq> frontier T" |
|
2549 apply (simp add: frontier_def) |
|
2550 using continuous_image_subset_interior assms(2) assms(3) S by auto |
|
2551 have "f ` interior S \<subseteq> interior T" |
|
2552 using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp |
|
2553 then have gim: "g ` frontier T \<subseteq> frontier S" |
|
2554 apply (simp add: frontier_def) |
|
2555 using continuous_image_subset_interior T assms(2) assms(3) by auto |
|
2556 show "homeomorphism (frontier S) (frontier T) f g" |
|
2557 unfolding homeomorphism_def |
|
2558 proof (intro conjI ballI) |
|
2559 show gf: "\<And>x. x \<in> frontier S \<Longrightarrow> g (f x) = x" |
|
2560 by (simp add: S assms(2) frontier_def) |
|
2561 show fg: "\<And>y. y \<in> frontier T \<Longrightarrow> f (g y) = y" |
|
2562 by (simp add: T assms(3) frontier_def) |
|
2563 have "frontier T \<subseteq> f ` frontier S" |
|
2564 proof |
|
2565 fix x assume "x \<in> frontier T" |
|
2566 then have "g x \<in> frontier S" |
|
2567 using gim by blast |
|
2568 then show "x \<in> f ` frontier S" |
|
2569 by (metis fg \<open>x \<in> frontier T\<close> imageI) |
|
2570 qed |
|
2571 then show "f ` frontier S = frontier T" |
|
2572 using fim by blast |
|
2573 show "continuous_on (frontier S) f" |
|
2574 by (metis Diff_subset assms(2) closure_eq contf continuous_on_subset frontier_def) |
|
2575 have "frontier S \<subseteq> g ` frontier T" |
|
2576 proof |
|
2577 fix x assume "x \<in> frontier S" |
|
2578 then have "f x \<in> frontier T" |
|
2579 using fim by blast |
|
2580 then show "x \<in> g ` frontier T" |
|
2581 by (metis gf \<open>x \<in> frontier S\<close> imageI) |
|
2582 qed |
|
2583 then show "g ` frontier T = frontier S" |
|
2584 using gim by blast |
|
2585 show "continuous_on (frontier T) g" |
|
2586 by (metis Diff_subset assms(3) closure_closed contg continuous_on_subset frontier_def) |
|
2587 qed |
|
2588 qed |
|
2589 |
|
2590 lemma homeomorphic_frontiers: |
|
2591 fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" |
|
2592 assumes "S homeomorphic T" "closed S" "closed T" |
|
2593 "interior S = {} \<longleftrightarrow> interior T = {}" |
|
2594 shows "(frontier S) homeomorphic (frontier T)" |
|
2595 proof (cases "interior T = {}") |
|
2596 case True |
|
2597 then show ?thesis |
|
2598 by (metis Diff_empty assms closure_eq frontier_def) |
|
2599 next |
|
2600 case False |
|
2601 show ?thesis |
|
2602 apply (rule homeomorphic_frontiers_same_dimension) |
|
2603 apply (simp_all add: assms) |
|
2604 using False assms homeomorphic_interiors homeomorphic_open_imp_same_dimension by blast |
|
2605 qed |
|
2606 |
|
2607 lemma continuous_image_subset_rel_interior: |
|
2608 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
2609 assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T" |
|
2610 and TS: "aff_dim T \<le> aff_dim S" |
|
2611 shows "f ` (rel_interior S) \<subseteq> rel_interior(f ` S)" |
|
2612 proof (rule rel_interior_maximal) |
|
2613 show "f ` rel_interior S \<subseteq> f ` S" |
|
2614 by(simp add: image_mono rel_interior_subset) |
|
2615 show "openin (top_of_set (affine hull f ` S)) (f ` rel_interior S)" |
|
2616 proof (rule invariance_of_domain_affine_sets) |
|
2617 show "openin (top_of_set (affine hull S)) (rel_interior S)" |
|
2618 by (simp add: openin_rel_interior) |
|
2619 show "aff_dim (affine hull f ` S) \<le> aff_dim (affine hull S)" |
|
2620 by (metis aff_dim_affine_hull aff_dim_subset fim TS order_trans) |
|
2621 show "f ` rel_interior S \<subseteq> affine hull f ` S" |
|
2622 by (meson \<open>f ` rel_interior S \<subseteq> f ` S\<close> hull_subset order_trans) |
|
2623 show "continuous_on (rel_interior S) f" |
|
2624 using contf continuous_on_subset rel_interior_subset by blast |
|
2625 show "inj_on f (rel_interior S)" |
|
2626 using inj_on_subset injf rel_interior_subset by blast |
|
2627 qed auto |
|
2628 qed |
|
2629 |
|
2630 lemma homeomorphic_rel_interiors_same_dimension: |
|
2631 fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" |
|
2632 assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T" |
|
2633 shows "(rel_interior S) homeomorphic (rel_interior T)" |
|
2634 using assms [unfolded homeomorphic_minimal] |
|
2635 unfolding homeomorphic_def |
|
2636 proof (clarify elim!: ex_forward) |
|
2637 fix f g |
|
2638 assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y" |
|
2639 and contf: "continuous_on S f" and contg: "continuous_on T g" |
|
2640 then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T" |
|
2641 by (auto simp: inj_on_def intro: rev_image_eqI) metis+ |
|
2642 have fim: "f ` rel_interior S \<subseteq> rel_interior T" |
|
2643 by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl) |
|
2644 have gim: "g ` rel_interior T \<subseteq> rel_interior S" |
|
2645 by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl) |
|
2646 show "homeomorphism (rel_interior S) (rel_interior T) f g" |
|
2647 unfolding homeomorphism_def |
|
2648 proof (intro conjI ballI) |
|
2649 show gf: "\<And>x. x \<in> rel_interior S \<Longrightarrow> g (f x) = x" |
|
2650 using S rel_interior_subset by blast |
|
2651 show fg: "\<And>y. y \<in> rel_interior T \<Longrightarrow> f (g y) = y" |
|
2652 using T mem_rel_interior_ball by blast |
|
2653 have "rel_interior T \<subseteq> f ` rel_interior S" |
|
2654 proof |
|
2655 fix x assume "x \<in> rel_interior T" |
|
2656 then have "g x \<in> rel_interior S" |
|
2657 using gim by blast |
|
2658 then show "x \<in> f ` rel_interior S" |
|
2659 by (metis fg \<open>x \<in> rel_interior T\<close> imageI) |
|
2660 qed |
|
2661 moreover have "f ` rel_interior S \<subseteq> rel_interior T" |
|
2662 by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl) |
|
2663 ultimately show "f ` rel_interior S = rel_interior T" |
|
2664 by blast |
|
2665 show "continuous_on (rel_interior S) f" |
|
2666 using contf continuous_on_subset rel_interior_subset by blast |
|
2667 have "rel_interior S \<subseteq> g ` rel_interior T" |
|
2668 proof |
|
2669 fix x assume "x \<in> rel_interior S" |
|
2670 then have "f x \<in> rel_interior T" |
|
2671 using fim by blast |
|
2672 then show "x \<in> g ` rel_interior T" |
|
2673 by (metis gf \<open>x \<in> rel_interior S\<close> imageI) |
|
2674 qed |
|
2675 then show "g ` rel_interior T = rel_interior S" |
|
2676 using gim by blast |
|
2677 show "continuous_on (rel_interior T) g" |
|
2678 using contg continuous_on_subset rel_interior_subset by blast |
|
2679 qed |
|
2680 qed |
|
2681 |
|
2682 lemma homeomorphic_rel_interiors: |
|
2683 fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" |
|
2684 assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}" |
|
2685 shows "(rel_interior S) homeomorphic (rel_interior T)" |
|
2686 proof (cases "rel_interior T = {}") |
|
2687 case True |
|
2688 with assms show ?thesis by auto |
|
2689 next |
|
2690 case False |
|
2691 obtain f g |
|
2692 where S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y" |
|
2693 and contf: "continuous_on S f" and contg: "continuous_on T g" |
|
2694 using assms [unfolded homeomorphic_minimal] by auto |
|
2695 have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)" |
|
2696 apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior S" _ f]) |
|
2697 apply (simp_all add: openin_rel_interior False assms) |
|
2698 using contf continuous_on_subset rel_interior_subset apply blast |
|
2699 apply (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD) |
|
2700 apply (metis S inj_on_inverseI inj_on_subset rel_interior_subset) |
|
2701 done |
|
2702 moreover have "aff_dim (affine hull T) \<le> aff_dim (affine hull S)" |
|
2703 apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior T" _ g]) |
|
2704 apply (simp_all add: openin_rel_interior False assms) |
|
2705 using contg continuous_on_subset rel_interior_subset apply blast |
|
2706 apply (meson T hull_subset image_subsetI rel_interior_subset rev_subsetD) |
|
2707 apply (metis T inj_on_inverseI inj_on_subset rel_interior_subset) |
|
2708 done |
|
2709 ultimately have "aff_dim S = aff_dim T" by force |
|
2710 then show ?thesis |
|
2711 by (rule homeomorphic_rel_interiors_same_dimension [OF \<open>S homeomorphic T\<close>]) |
|
2712 qed |
|
2713 |
|
2714 |
|
2715 lemma homeomorphic_rel_boundaries_same_dimension: |
|
2716 fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" |
|
2717 assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T" |
|
2718 shows "(S - rel_interior S) homeomorphic (T - rel_interior T)" |
|
2719 using assms [unfolded homeomorphic_minimal] |
|
2720 unfolding homeomorphic_def |
|
2721 proof (clarify elim!: ex_forward) |
|
2722 fix f g |
|
2723 assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y" |
|
2724 and contf: "continuous_on S f" and contg: "continuous_on T g" |
|
2725 then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T" |
|
2726 by (auto simp: inj_on_def intro: rev_image_eqI) metis+ |
|
2727 have fim: "f ` rel_interior S \<subseteq> rel_interior T" |
|
2728 by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl) |
|
2729 have gim: "g ` rel_interior T \<subseteq> rel_interior S" |
|
2730 by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl) |
|
2731 show "homeomorphism (S - rel_interior S) (T - rel_interior T) f g" |
|
2732 unfolding homeomorphism_def |
|
2733 proof (intro conjI ballI) |
|
2734 show gf: "\<And>x. x \<in> S - rel_interior S \<Longrightarrow> g (f x) = x" |
|
2735 using S rel_interior_subset by blast |
|
2736 show fg: "\<And>y. y \<in> T - rel_interior T \<Longrightarrow> f (g y) = y" |
|
2737 using T mem_rel_interior_ball by blast |
|
2738 show "f ` (S - rel_interior S) = T - rel_interior T" |
|
2739 using S fST fim gim by auto |
|
2740 show "continuous_on (S - rel_interior S) f" |
|
2741 using contf continuous_on_subset rel_interior_subset by blast |
|
2742 show "g ` (T - rel_interior T) = S - rel_interior S" |
|
2743 using T gTS gim fim by auto |
|
2744 show "continuous_on (T - rel_interior T) g" |
|
2745 using contg continuous_on_subset rel_interior_subset by blast |
|
2746 qed |
|
2747 qed |
|
2748 |
|
2749 lemma homeomorphic_rel_boundaries: |
|
2750 fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" |
|
2751 assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}" |
|
2752 shows "(S - rel_interior S) homeomorphic (T - rel_interior T)" |
|
2753 proof (cases "rel_interior T = {}") |
|
2754 case True |
|
2755 with assms show ?thesis by auto |
|
2756 next |
|
2757 case False |
|
2758 obtain f g |
|
2759 where S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y" |
|
2760 and contf: "continuous_on S f" and contg: "continuous_on T g" |
|
2761 using assms [unfolded homeomorphic_minimal] by auto |
|
2762 have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)" |
|
2763 apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior S" _ f]) |
|
2764 apply (simp_all add: openin_rel_interior False assms) |
|
2765 using contf continuous_on_subset rel_interior_subset apply blast |
|
2766 apply (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD) |
|
2767 apply (metis S inj_on_inverseI inj_on_subset rel_interior_subset) |
|
2768 done |
|
2769 moreover have "aff_dim (affine hull T) \<le> aff_dim (affine hull S)" |
|
2770 apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior T" _ g]) |
|
2771 apply (simp_all add: openin_rel_interior False assms) |
|
2772 using contg continuous_on_subset rel_interior_subset apply blast |
|
2773 apply (meson T hull_subset image_subsetI rel_interior_subset rev_subsetD) |
|
2774 apply (metis T inj_on_inverseI inj_on_subset rel_interior_subset) |
|
2775 done |
|
2776 ultimately have "aff_dim S = aff_dim T" by force |
|
2777 then show ?thesis |
|
2778 by (rule homeomorphic_rel_boundaries_same_dimension [OF \<open>S homeomorphic T\<close>]) |
|
2779 qed |
|
2780 |
|
2781 proposition uniformly_continuous_homeomorphism_UNIV_trivial: |
|
2782 fixes f :: "'a::euclidean_space \<Rightarrow> 'a" |
|
2783 assumes contf: "uniformly_continuous_on S f" and hom: "homeomorphism S UNIV f g" |
|
2784 shows "S = UNIV" |
|
2785 proof (cases "S = {}") |
|
2786 case True |
|
2787 then show ?thesis |
|
2788 by (metis UNIV_I hom empty_iff homeomorphism_def image_eqI) |
|
2789 next |
|
2790 case False |
|
2791 have "inj g" |
|
2792 by (metis UNIV_I hom homeomorphism_apply2 injI) |
|
2793 then have "open (g ` UNIV)" |
|
2794 by (blast intro: invariance_of_domain hom homeomorphism_cont2) |
|
2795 then have "open S" |
|
2796 using hom homeomorphism_image2 by blast |
|
2797 moreover have "complete S" |
|
2798 unfolding complete_def |
|
2799 proof clarify |
|
2800 fix \<sigma> |
|
2801 assume \<sigma>: "\<forall>n. \<sigma> n \<in> S" and "Cauchy \<sigma>" |
|
2802 have "Cauchy (f o \<sigma>)" |
|
2803 using uniformly_continuous_imp_Cauchy_continuous \<open>Cauchy \<sigma>\<close> \<sigma> contf by blast |
|
2804 then obtain l where "(f \<circ> \<sigma>) \<longlonglongrightarrow> l" |
|
2805 by (auto simp: convergent_eq_Cauchy [symmetric]) |
|
2806 show "\<exists>l\<in>S. \<sigma> \<longlonglongrightarrow> l" |
|
2807 proof |
|
2808 show "g l \<in> S" |
|
2809 using hom homeomorphism_image2 by blast |
|
2810 have "(g \<circ> (f \<circ> \<sigma>)) \<longlonglongrightarrow> g l" |
|
2811 by (meson UNIV_I \<open>(f \<circ> \<sigma>) \<longlonglongrightarrow> l\<close> continuous_on_sequentially hom homeomorphism_cont2) |
|
2812 then show "\<sigma> \<longlonglongrightarrow> g l" |
|
2813 proof - |
|
2814 have "\<forall>n. \<sigma> n = (g \<circ> (f \<circ> \<sigma>)) n" |
|
2815 by (metis (no_types) \<sigma> comp_eq_dest_lhs hom homeomorphism_apply1) |
|
2816 then show ?thesis |
|
2817 by (metis (no_types) LIMSEQ_iff \<open>(g \<circ> (f \<circ> \<sigma>)) \<longlonglongrightarrow> g l\<close>) |
|
2818 qed |
|
2819 qed |
|
2820 qed |
|
2821 then have "closed S" |
|
2822 by (simp add: complete_eq_closed) |
|
2823 ultimately show ?thesis |
|
2824 using clopen [of S] False by simp |
|
2825 qed |
|
2826 |
|
2827 proposition invariance_of_domain_sphere_affine_set_gen: |
|
2828 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
2829 assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T" |
|
2830 and U: "bounded U" "convex U" |
|
2831 and "affine T" and affTU: "aff_dim T < aff_dim U" |
|
2832 and ope: "openin (top_of_set (rel_frontier U)) S" |
|
2833 shows "openin (top_of_set T) (f ` S)" |
|
2834 proof (cases "rel_frontier U = {}") |
|
2835 case True |
|
2836 then show ?thesis |
|
2837 using ope openin_subset by force |
|
2838 next |
|
2839 case False |
|
2840 obtain b c where b: "b \<in> rel_frontier U" and c: "c \<in> rel_frontier U" and "b \<noteq> c" |
|
2841 using \<open>bounded U\<close> rel_frontier_not_sing [of U] subset_singletonD False by fastforce |
|
2842 obtain V :: "'a set" where "affine V" and affV: "aff_dim V = aff_dim U - 1" |
|
2843 proof (rule choose_affine_subset [OF affine_UNIV]) |
|
2844 show "- 1 \<le> aff_dim U - 1" |
|
2845 by (metis aff_dim_empty aff_dim_geq aff_dim_negative_iff affTU diff_0 diff_right_mono not_le) |
|
2846 show "aff_dim U - 1 \<le> aff_dim (UNIV::'a set)" |
|
2847 by (metis aff_dim_UNIV aff_dim_le_DIM le_cases not_le zle_diff1_eq) |
|
2848 qed auto |
|
2849 have SU: "S \<subseteq> rel_frontier U" |
|
2850 using ope openin_imp_subset by auto |
|
2851 have homb: "rel_frontier U - {b} homeomorphic V" |
|
2852 and homc: "rel_frontier U - {c} homeomorphic V" |
|
2853 using homeomorphic_punctured_sphere_affine_gen [of U _ V] |
|
2854 by (simp_all add: \<open>affine V\<close> affV U b c) |
|
2855 then obtain g h j k |
|
2856 where gh: "homeomorphism (rel_frontier U - {b}) V g h" |
|
2857 and jk: "homeomorphism (rel_frontier U - {c}) V j k" |
|
2858 by (auto simp: homeomorphic_def) |
|
2859 with SU have hgsub: "(h ` g ` (S - {b})) \<subseteq> S" and kjsub: "(k ` j ` (S - {c})) \<subseteq> S" |
|
2860 by (simp_all add: homeomorphism_def subset_eq) |
|
2861 have [simp]: "aff_dim T \<le> aff_dim V" |
|
2862 by (simp add: affTU affV) |
|
2863 have "openin (top_of_set T) ((f \<circ> h) ` g ` (S - {b}))" |
|
2864 proof (rule invariance_of_domain_affine_sets [OF _ \<open>affine V\<close>]) |
|
2865 show "openin (top_of_set V) (g ` (S - {b}))" |
|
2866 apply (rule homeomorphism_imp_open_map [OF gh]) |
|
2867 by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl) |
|
2868 show "continuous_on (g ` (S - {b})) (f \<circ> h)" |
|
2869 apply (rule continuous_on_compose) |
|
2870 apply (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets gh set_eq_subset) |
|
2871 using contf continuous_on_subset hgsub by blast |
|
2872 show "inj_on (f \<circ> h) (g ` (S - {b}))" |
|
2873 using kjsub |
|
2874 apply (clarsimp simp add: inj_on_def) |
|
2875 by (metis SU b homeomorphism_def inj_onD injf insert_Diff insert_iff gh rev_subsetD) |
|
2876 show "(f \<circ> h) ` g ` (S - {b}) \<subseteq> T" |
|
2877 by (metis fim image_comp image_mono hgsub subset_trans) |
|
2878 qed (auto simp: assms) |
|
2879 moreover |
|
2880 have "openin (top_of_set T) ((f \<circ> k) ` j ` (S - {c}))" |
|
2881 proof (rule invariance_of_domain_affine_sets [OF _ \<open>affine V\<close>]) |
|
2882 show "openin (top_of_set V) (j ` (S - {c}))" |
|
2883 apply (rule homeomorphism_imp_open_map [OF jk]) |
|
2884 by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl) |
|
2885 show "continuous_on (j ` (S - {c})) (f \<circ> k)" |
|
2886 apply (rule continuous_on_compose) |
|
2887 apply (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets jk set_eq_subset) |
|
2888 using contf continuous_on_subset kjsub by blast |
|
2889 show "inj_on (f \<circ> k) (j ` (S - {c}))" |
|
2890 using kjsub |
|
2891 apply (clarsimp simp add: inj_on_def) |
|
2892 by (metis SU c homeomorphism_def inj_onD injf insert_Diff insert_iff jk rev_subsetD) |
|
2893 show "(f \<circ> k) ` j ` (S - {c}) \<subseteq> T" |
|
2894 by (metis fim image_comp image_mono kjsub subset_trans) |
|
2895 qed (auto simp: assms) |
|
2896 ultimately have "openin (top_of_set T) ((f \<circ> h) ` g ` (S - {b}) \<union> ((f \<circ> k) ` j ` (S - {c})))" |
|
2897 by (rule openin_Un) |
|
2898 moreover have "(f \<circ> h) ` g ` (S - {b}) = f ` (S - {b})" |
|
2899 proof - |
|
2900 have "h ` g ` (S - {b}) = (S - {b})" |
|
2901 proof |
|
2902 show "h ` g ` (S - {b}) \<subseteq> S - {b}" |
|
2903 using homeomorphism_apply1 [OF gh] SU |
|
2904 by (fastforce simp add: image_iff image_subset_iff) |
|
2905 show "S - {b} \<subseteq> h ` g ` (S - {b})" |
|
2906 apply clarify |
|
2907 by (metis SU subsetD homeomorphism_apply1 [OF gh] image_iff member_remove remove_def) |
|
2908 qed |
|
2909 then show ?thesis |
|
2910 by (metis image_comp) |
|
2911 qed |
|
2912 moreover have "(f \<circ> k) ` j ` (S - {c}) = f ` (S - {c})" |
|
2913 proof - |
|
2914 have "k ` j ` (S - {c}) = (S - {c})" |
|
2915 proof |
|
2916 show "k ` j ` (S - {c}) \<subseteq> S - {c}" |
|
2917 using homeomorphism_apply1 [OF jk] SU |
|
2918 by (fastforce simp add: image_iff image_subset_iff) |
|
2919 show "S - {c} \<subseteq> k ` j ` (S - {c})" |
|
2920 apply clarify |
|
2921 by (metis SU subsetD homeomorphism_apply1 [OF jk] image_iff member_remove remove_def) |
|
2922 qed |
|
2923 then show ?thesis |
|
2924 by (metis image_comp) |
|
2925 qed |
|
2926 moreover have "f ` (S - {b}) \<union> f ` (S - {c}) = f ` (S)" |
|
2927 using \<open>b \<noteq> c\<close> by blast |
|
2928 ultimately show ?thesis |
|
2929 by simp |
|
2930 qed |
|
2931 |
|
2932 lemma invariance_of_domain_sphere_affine_set: |
|
2933 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
2934 assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T" |
|
2935 and "r \<noteq> 0" "affine T" and affTU: "aff_dim T < DIM('a)" |
|
2936 and ope: "openin (top_of_set (sphere a r)) S" |
|
2937 shows "openin (top_of_set T) (f ` S)" |
|
2938 proof (cases "sphere a r = {}") |
|
2939 case True |
|
2940 then show ?thesis |
|
2941 using ope openin_subset by force |
|
2942 next |
|
2943 case False |
|
2944 show ?thesis |
|
2945 proof (rule invariance_of_domain_sphere_affine_set_gen [OF contf injf fim bounded_cball convex_cball \<open>affine T\<close>]) |
|
2946 show "aff_dim T < aff_dim (cball a r)" |
|
2947 by (metis False affTU aff_dim_cball assms(4) linorder_cases sphere_empty) |
|
2948 show "openin (top_of_set (rel_frontier (cball a r))) S" |
|
2949 by (simp add: \<open>r \<noteq> 0\<close> ope) |
|
2950 qed |
|
2951 qed |
|
2952 |
|
2953 lemma no_embedding_sphere_lowdim: |
|
2954 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
2955 assumes contf: "continuous_on (sphere a r) f" and injf: "inj_on f (sphere a r)" and "r > 0" |
|
2956 shows "DIM('a) \<le> DIM('b)" |
|
2957 proof - |
|
2958 have "False" if "DIM('a) > DIM('b)" |
|
2959 proof - |
|
2960 have "compact (f ` sphere a r)" |
|
2961 using compact_continuous_image |
|
2962 by (simp add: compact_continuous_image contf) |
|
2963 then have "\<not> open (f ` sphere a r)" |
|
2964 using compact_open |
|
2965 by (metis assms(3) image_is_empty not_less_iff_gr_or_eq sphere_eq_empty) |
|
2966 then show False |
|
2967 using invariance_of_domain_sphere_affine_set [OF contf injf subset_UNIV] \<open>r > 0\<close> |
|
2968 by (metis aff_dim_UNIV affine_UNIV less_irrefl of_nat_less_iff open_openin openin_subtopology_self subtopology_UNIV that) |
|
2969 qed |
|
2970 then show ?thesis |
|
2971 using not_less by blast |
|
2972 qed |
|
2973 |
2429 end |
2974 end |