60 by (simp add: \<open>g \<circ> f = id\<close> S image_comp) |
60 by (simp add: \<open>g \<circ> f = id\<close> S image_comp) |
61 have [simp]: "(range f \<inter> g -` S) = f ` S" |
61 have [simp]: "(range f \<inter> g -` S) = f ` S" |
62 using g unfolding o_def id_def image_def by auto metis+ |
62 using g unfolding o_def id_def image_def by auto metis+ |
63 show ?thesis |
63 show ?thesis |
64 proof (rule closedin_closed_trans [of "range f"]) |
64 proof (rule closedin_closed_trans [of "range f"]) |
65 show "closedin (subtopology euclidean (range f)) (f ` S)" |
65 show "closedin (top_of_set (range f)) (f ` S)" |
66 using continuous_closedin_preimage [OF confg cgf] by simp |
66 using continuous_closedin_preimage [OF confg cgf] by simp |
67 show "closed (range f)" |
67 show "closed (range f)" |
68 apply (rule closed_injective_image_subspace) |
68 apply (rule closed_injective_image_subspace) |
69 using f apply (auto simp: linear_linear linear_injective_0) |
69 using f apply (auto simp: linear_linear linear_injective_0) |
70 done |
70 done |
317 |
317 |
318 |
318 |
319 subsection \<open>Relative interior of a set\<close> |
319 subsection \<open>Relative interior of a set\<close> |
320 |
320 |
321 definition%important "rel_interior S = |
321 definition%important "rel_interior S = |
322 {x. \<exists>T. openin (subtopology euclidean (affine hull S)) T \<and> x \<in> T \<and> T \<subseteq> S}" |
322 {x. \<exists>T. openin (top_of_set (affine hull S)) T \<and> x \<in> T \<and> T \<subseteq> S}" |
323 |
323 |
324 lemma rel_interior_mono: |
324 lemma rel_interior_mono: |
325 "\<lbrakk>S \<subseteq> T; affine hull S = affine hull T\<rbrakk> |
325 "\<lbrakk>S \<subseteq> T; affine hull S = affine hull T\<rbrakk> |
326 \<Longrightarrow> (rel_interior S) \<subseteq> (rel_interior T)" |
326 \<Longrightarrow> (rel_interior S) \<subseteq> (rel_interior T)" |
327 by (auto simp: rel_interior_def) |
327 by (auto simp: rel_interior_def) |
328 |
328 |
329 lemma rel_interior_maximal: |
329 lemma rel_interior_maximal: |
330 "\<lbrakk>T \<subseteq> S; openin(subtopology euclidean (affine hull S)) T\<rbrakk> \<Longrightarrow> T \<subseteq> (rel_interior S)" |
330 "\<lbrakk>T \<subseteq> S; openin(top_of_set (affine hull S)) T\<rbrakk> \<Longrightarrow> T \<subseteq> (rel_interior S)" |
331 by (auto simp: rel_interior_def) |
331 by (auto simp: rel_interior_def) |
332 |
332 |
333 lemma rel_interior: |
333 lemma rel_interior: |
334 "rel_interior S = {x \<in> S. \<exists>T. open T \<and> x \<in> T \<and> T \<inter> affine hull S \<subseteq> S}" |
334 "rel_interior S = {x \<in> S. \<exists>T. open T \<and> x \<in> T \<and> T \<inter> affine hull S \<subseteq> S}" |
335 unfolding rel_interior_def[of S] openin_open[of "affine hull S"] |
335 unfolding rel_interior_def[of S] openin_open[of "affine hull S"] |
649 |
649 |
650 subsubsection \<open>Relative open sets\<close> |
650 subsubsection \<open>Relative open sets\<close> |
651 |
651 |
652 definition%important "rel_open S \<longleftrightarrow> rel_interior S = S" |
652 definition%important "rel_open S \<longleftrightarrow> rel_interior S = S" |
653 |
653 |
654 lemma rel_open: "rel_open S \<longleftrightarrow> openin (subtopology euclidean (affine hull S)) S" |
654 lemma rel_open: "rel_open S \<longleftrightarrow> openin (top_of_set (affine hull S)) S" |
655 unfolding rel_open_def rel_interior_def |
655 unfolding rel_open_def rel_interior_def |
656 apply auto |
656 apply auto |
657 using openin_subopen[of "subtopology euclidean (affine hull S)" S] |
657 using openin_subopen[of "top_of_set (affine hull S)" S] |
658 apply auto |
658 apply auto |
659 done |
659 done |
660 |
660 |
661 lemma openin_rel_interior: "openin (subtopology euclidean (affine hull S)) (rel_interior S)" |
661 lemma openin_rel_interior: "openin (top_of_set (affine hull S)) (rel_interior S)" |
662 apply (simp add: rel_interior_def) |
662 apply (simp add: rel_interior_def) |
663 apply (subst openin_subopen, blast) |
663 apply (subst openin_subopen, blast) |
664 done |
664 done |
665 |
665 |
666 lemma openin_set_rel_interior: |
666 lemma openin_set_rel_interior: |
667 "openin (subtopology euclidean S) (rel_interior S)" |
667 "openin (top_of_set S) (rel_interior S)" |
668 by (rule openin_subset_trans [OF openin_rel_interior rel_interior_subset hull_subset]) |
668 by (rule openin_subset_trans [OF openin_rel_interior rel_interior_subset hull_subset]) |
669 |
669 |
670 lemma affine_rel_open: |
670 lemma affine_rel_open: |
671 fixes S :: "'n::euclidean_space set" |
671 fixes S :: "'n::euclidean_space set" |
672 assumes "affine S" |
672 assumes "affine S" |
804 using rel_interior_convex_shrink[of S z y e] assms \<open>y \<in> S\<close> by auto |
804 using rel_interior_convex_shrink[of S z y e] assms \<open>y \<in> S\<close> by auto |
805 then show ?thesis using * by auto |
805 then show ?thesis using * by auto |
806 qed |
806 qed |
807 |
807 |
808 lemma rel_interior_eq: |
808 lemma rel_interior_eq: |
809 "rel_interior s = s \<longleftrightarrow> openin(subtopology euclidean (affine hull s)) s" |
809 "rel_interior s = s \<longleftrightarrow> openin(top_of_set (affine hull s)) s" |
810 using rel_open rel_open_def by blast |
810 using rel_open rel_open_def by blast |
811 |
811 |
812 lemma rel_interior_openin: |
812 lemma rel_interior_openin: |
813 "openin(subtopology euclidean (affine hull s)) s \<Longrightarrow> rel_interior s = s" |
813 "openin(top_of_set (affine hull s)) s \<Longrightarrow> rel_interior s = s" |
814 by (simp add: rel_interior_eq) |
814 by (simp add: rel_interior_eq) |
815 |
815 |
816 lemma rel_interior_affine: |
816 lemma rel_interior_affine: |
817 fixes S :: "'n::euclidean_space set" |
817 fixes S :: "'n::euclidean_space set" |
818 shows "affine S \<Longrightarrow> rel_interior S = S" |
818 shows "affine S \<Longrightarrow> rel_interior S = S" |
1990 proof - |
1990 proof - |
1991 have False if "a \<in> T" "open T" "\<And>y. \<lbrakk>y \<in> S; y \<in> T\<rbrakk> \<Longrightarrow> y = a" for T |
1991 have False if "a \<in> T" "open T" "\<And>y. \<lbrakk>y \<in> S; y \<in> T\<rbrakk> \<Longrightarrow> y = a" for T |
1992 proof - |
1992 proof - |
1993 obtain e where "e > 0" and e: "cball a e \<subseteq> T" |
1993 obtain e where "e > 0" and e: "cball a e \<subseteq> T" |
1994 using \<open>open T\<close> \<open>a \<in> T\<close> by (auto simp: open_contains_cball) |
1994 using \<open>open T\<close> \<open>a \<in> T\<close> by (auto simp: open_contains_cball) |
1995 have "openin (subtopology euclidean S) {a}" |
1995 have "openin (top_of_set S) {a}" |
1996 unfolding openin_open using that \<open>a \<in> S\<close> by blast |
1996 unfolding openin_open using that \<open>a \<in> S\<close> by blast |
1997 moreover have "closedin (subtopology euclidean S) {a}" |
1997 moreover have "closedin (top_of_set S) {a}" |
1998 by (simp add: assms) |
1998 by (simp add: assms) |
1999 ultimately show "False" |
1999 ultimately show "False" |
2000 using \<open>connected S\<close> connected_clopen S by blast |
2000 using \<open>connected S\<close> connected_clopen S by blast |
2001 qed |
2001 qed |
2002 then show ?thesis |
2002 then show ?thesis |