Added embedding_map_into_euclideanreal; reduced dependence on Equivalence_Lebesgue_Henstock_Integration in Analysis theories by moving a few lemmas
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Apr 25 10:19:48 2019 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Fri Apr 26 16:51:40 2019 +0100
@@ -3,9 +3,40 @@
text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close>
theory Cauchy_Integral_Theorem
-imports Complex_Transcendental Weierstrass_Theorems Ordered_Euclidean_Space
+imports Complex_Transcendental Henstock_Kurzweil_Integration Weierstrass_Theorems Ordered_Euclidean_Space
begin
+lemma leibniz_rule_holomorphic:
+ fixes f::"complex \<Rightarrow> 'b::euclidean_space \<Rightarrow> complex"
+ assumes "\<And>x t. x \<in> U \<Longrightarrow> t \<in> cbox a b \<Longrightarrow> ((\<lambda>x. f x t) has_field_derivative fx x t) (at x within U)"
+ assumes "\<And>x. x \<in> U \<Longrightarrow> (f x) integrable_on cbox a b"
+ assumes "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)"
+ assumes "convex U"
+ shows "(\<lambda>x. integral (cbox a b) (f x)) holomorphic_on U"
+ using leibniz_rule_field_differentiable[OF assms(1-3) _ assms(4)]
+ by (auto simp: holomorphic_on_def)
+
+lemma Ln_measurable [measurable]: "Ln \<in> measurable borel borel"
+proof -
+ have *: "Ln (-of_real x) = of_real (ln x) + \<i> * pi" if "x > 0" for x
+ using that by (subst Ln_minus) (auto simp: Ln_of_real)
+ have **: "Ln (of_real x) = of_real (ln (-x)) + \<i> * pi" if "x < 0" for x
+ using *[of "-x"] that by simp
+ have cont: "(\<lambda>x. indicat_real (- \<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel_measurable borel"
+ by (intro borel_measurable_continuous_on_indicator continuous_intros) auto
+ have "(\<lambda>x. if x \<in> \<real>\<^sub>\<le>\<^sub>0 then ln (-Re x) + \<i> * pi else indicator (-\<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel \<rightarrow>\<^sub>M borel"
+ (is "?f \<in> _") by (rule measurable_If_set[OF _ cont]) auto
+ hence "(\<lambda>x. if x = 0 then Ln 0 else ?f x) \<in> borel \<rightarrow>\<^sub>M borel" by measurable
+ also have "(\<lambda>x. if x = 0 then Ln 0 else ?f x) = Ln"
+ by (auto simp: fun_eq_iff ** nonpos_Reals_def)
+ finally show ?thesis .
+qed
+
+lemma powr_complex_measurable [measurable]:
+ assumes [measurable]: "f \<in> measurable M borel" "g \<in> measurable M borel"
+ shows "(\<lambda>x. f x powr g x :: complex) \<in> measurable M borel"
+ using assms by (simp add: powr_def)
+
subsection\<^marker>\<open>tag unimportant\<close> \<open>Homeomorphisms of arc images\<close>
lemma homeomorphism_arc:
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Apr 25 10:19:48 2019 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Fri Apr 26 16:51:40 2019 +0100
@@ -5,7 +5,7 @@
section \<open>Complex Analysis Basics\<close>
theory Complex_Analysis_Basics
-imports Equivalence_Lebesgue_Henstock_Integration "HOL-Library.Nonpos_Ints"
+ imports Derivative "HOL-Library.Nonpos_Ints"
begin
(* TODO FIXME: A lot of the things in here have nothing to do with complex analysis *)
@@ -83,31 +83,6 @@
lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
by (intro continuous_on_id continuous_on_norm)
-(*MOVE? But not to Finite_Cartesian_Product*)
-lemma sums_vec_nth :
- assumes "f sums a"
- shows "(\<lambda>x. f x $ i) sums a $ i"
-using assms unfolding sums_def
-by (auto dest: tendsto_vec_nth [where i=i])
-
-lemma summable_vec_nth :
- assumes "summable f"
- shows "summable (\<lambda>x. f x $ i)"
-using assms unfolding summable_def
-by (blast intro: sums_vec_nth)
-
-(* TODO: Move? *)
-lemma DERIV_zero_connected_constant:
- fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
- assumes "connected S"
- and "open S"
- and "finite K"
- and "continuous_on S f"
- and "\<forall>x\<in>(S - K). DERIV f x :> 0"
- obtains c where "\<And>x. x \<in> S \<Longrightarrow> f(x) = c"
-using has_derivative_zero_connected_constant [OF assms(1-4)] assms
-by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def)
-
lemmas DERIV_zero_constant = has_field_derivative_zero_constant
lemma DERIV_zero_unique:
@@ -394,16 +369,6 @@
finally show \<dots> .
qed (insert assms, auto)
-lemma leibniz_rule_holomorphic:
- fixes f::"complex \<Rightarrow> 'b::euclidean_space \<Rightarrow> complex"
- assumes "\<And>x t. x \<in> U \<Longrightarrow> t \<in> cbox a b \<Longrightarrow> ((\<lambda>x. f x t) has_field_derivative fx x t) (at x within U)"
- assumes "\<And>x. x \<in> U \<Longrightarrow> (f x) integrable_on cbox a b"
- assumes "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)"
- assumes "convex U"
- shows "(\<lambda>x. integral (cbox a b) (f x)) holomorphic_on U"
- using leibniz_rule_field_differentiable[OF assms(1-3) _ assms(4)]
- by (auto simp: holomorphic_on_def)
-
lemma DERIV_deriv_iff_field_differentiable:
"DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
unfolding field_differentiable_def by (metis DERIV_imp_deriv)
--- a/src/HOL/Analysis/Complex_Transcendental.thy Thu Apr 25 10:19:48 2019 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Fri Apr 26 16:51:40 2019 +0100
@@ -4,9 +4,7 @@
theory Complex_Transcendental
imports
- Complex_Analysis_Basics
- Summation_Tests
- "HOL-Library.Periodic_Fun"
+ Complex_Analysis_Basics Summation_Tests "HOL-Library.Periodic_Fun"
begin
subsection\<open>Möbius transformations\<close>
@@ -875,7 +873,7 @@
have zr: "z = (cmod z) * exp (\<i> * r)" and zs: "z = (cmod z) * exp (\<i> * s)"
using r s by (auto simp: is_Arg_def)
with \<open>z \<noteq> 0\<close> have eq: "exp (\<i> * r) = exp (\<i> * s)"
- by (metis mult_eq_0_iff vector_space_over_itself.scale_left_imp_eq)
+ by (metis mult_eq_0_iff mult_left_cancel)
have "\<i> * r = \<i> * s"
by (rule exp_complex_eqI) (use rs in \<open>auto simp: eq exp_complex_eqI\<close>)
then show ?thesis
@@ -1728,27 +1726,6 @@
finally show ?thesis .
qed
-lemma Ln_measurable [measurable]: "Ln \<in> measurable borel borel"
-proof -
- have *: "Ln (-of_real x) = of_real (ln x) + \<i> * pi" if "x > 0" for x
- using that by (subst Ln_minus) (auto simp: Ln_of_real)
- have **: "Ln (of_real x) = of_real (ln (-x)) + \<i> * pi" if "x < 0" for x
- using *[of "-x"] that by simp
- have cont: "(\<lambda>x. indicat_real (- \<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on_indicator continuous_intros) auto
- have "(\<lambda>x. if x \<in> \<real>\<^sub>\<le>\<^sub>0 then ln (-Re x) + \<i> * pi else indicator (-\<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel \<rightarrow>\<^sub>M borel"
- (is "?f \<in> _") by (rule measurable_If_set[OF _ cont]) auto
- hence "(\<lambda>x. if x = 0 then Ln 0 else ?f x) \<in> borel \<rightarrow>\<^sub>M borel" by measurable
- also have "(\<lambda>x. if x = 0 then Ln 0 else ?f x) = Ln"
- by (auto simp: fun_eq_iff ** nonpos_Reals_def)
- finally show ?thesis .
-qed
-
-lemma powr_complex_measurable [measurable]:
- assumes [measurable]: "f \<in> measurable M borel" "g \<in> measurable M borel"
- shows "(\<lambda>x. f x powr g x :: complex) \<in> measurable M borel"
- using assms by (simp add: powr_def)
-
subsection\<open>The Argument of a Complex Number\<close>
text\<open>Finally: it's is defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close>
--- a/src/HOL/Analysis/Further_Topology.thy Thu Apr 25 10:19:48 2019 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy Fri Apr 26 16:51:40 2019 +0100
@@ -3,7 +3,7 @@
text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
theory Further_Topology
- imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope Complex_Transcendental
+ imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration
begin
subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
@@ -4644,8 +4644,8 @@
proof (rule upper_lower_hemicontinuous_explicit [of T "\<lambda>y. {z \<in> S. f z = y}" S])
show "\<And>U. openin (top_of_set S) U
\<Longrightarrow> openin (top_of_set T) {x \<in> T. {z \<in> S. f z = x} \<subseteq> U}"
- using continuous_imp_closed_map closed_map_iff_upper_hemicontinuous_preimage [OF fim [THEN equalityD1]]
- by (simp add: continuous_imp_closed_map \<open>compact S\<close> contf fim)
+ using closed_map_iff_upper_hemicontinuous_preimage [OF fim [THEN equalityD1]]
+ by (simp add: Abstract_Topology_2.continuous_imp_closed_map \<open>compact S\<close> contf fim)
show "\<And>U. closedin (top_of_set S) U \<Longrightarrow>
closedin (top_of_set T) {x \<in> T. {z \<in> S. f z = x} \<subseteq> U}"
using ope open_map_iff_lower_hemicontinuous_preimage [OF fim [THEN equalityD1]]
--- a/src/HOL/Analysis/Gamma_Function.thy Thu Apr 25 10:19:48 2019 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Fri Apr 26 16:51:40 2019 +0100
@@ -5,8 +5,9 @@
section \<open>The Gamma Function\<close>
theory Gamma_Function
-imports
+ imports
Conformal_Mappings
+ Equivalence_Lebesgue_Henstock_Integration
Summation_Tests
Harmonic_Numbers
"HOL-Library.Nonpos_Ints"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Apr 25 10:19:48 2019 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Apr 26 16:51:40 2019 +0100
@@ -7,8 +7,7 @@
theory Henstock_Kurzweil_Integration
imports
- Lebesgue_Measure
- Tagged_Division
+ Lebesgue_Measure Tagged_Division
begin
lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
@@ -4436,7 +4435,7 @@
proof (cases "S = {}")
case True
then show ?thesis
-by (metis empty_iff that)
+ by (metis empty_iff that)
next
case False
then obtain c where "c \<in> S"
@@ -4445,6 +4444,17 @@
by (metis has_derivative_zero_unique_strong_connected assms that)
qed
+lemma DERIV_zero_connected_constant:
+ fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
+ assumes "connected S"
+ and "open S"
+ and "finite K"
+ and "continuous_on S f"
+ and "\<forall>x\<in>(S - K). DERIV f x :> 0"
+ obtains c where "\<And>x. x \<in> S \<Longrightarrow> f(x) = c"
+ using has_derivative_zero_connected_constant [OF assms(1-4)] assms
+ by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def)
+
subsection \<open>Integrating characteristic function of an interval\<close>
--- a/src/HOL/Analysis/Homotopy.thy Thu Apr 25 10:19:48 2019 +0200
+++ b/src/HOL/Analysis/Homotopy.thy Fri Apr 26 16:51:40 2019 +0100
@@ -5655,22 +5655,20 @@
by auto
let ?h = "\<lambda>y. g (a + (fst y) *\<^sub>R (snd y - a))"
have "continuous_on ({0..1} \<times> sphere a r) ?h"
- apply (rule continuous_on_compose2 [OF contg])
- apply (intro continuous_intros)
- apply (auto simp: dist_norm norm_minus_commute mult_left_le_one_le)
- done
+ proof (rule continuous_on_compose2 [OF contg])
+ show "continuous_on ({0..1} \<times> sphere a r) (\<lambda>x. a + fst x *\<^sub>R (snd x - a))"
+ by (intro continuous_intros)
+ qed (auto simp: dist_norm norm_minus_commute mult_left_le_one_le)
moreover
have "?h ` ({0..1} \<times> sphere a r) \<subseteq> S"
by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gim [THEN subsetD])
moreover
have "\<forall>x\<in>sphere a r. ?h (0, x) = g a" "\<forall>x\<in>sphere a r. ?h (1, x) = f x"
by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gf)
- ultimately
- show ?lhs
- apply (subst homotopic_with_sym)
- apply (rule_tac x="g a" in exI)
- apply (auto simp: homotopic_with)
- done
+ ultimately have "homotopic_with_canon (\<lambda>x. True) (sphere a r) S (\<lambda>x. g a) f"
+ by (auto simp: homotopic_with)
+ then show ?lhs
+ using homotopic_with_symD by blast
qed
ultimately
show ?thesis by meson
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Thu Apr 25 10:19:48 2019 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Fri Apr 26 16:51:40 2019 +0100
@@ -188,6 +188,18 @@
shows "(\<lambda>x::real^1. x $ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)"
by (metis interval_cbox vec_nth_1_iff_cbox)
+lemma sums_vec_nth :
+ assumes "f sums a"
+ shows "(\<lambda>x. f x $ i) sums a $ i"
+ using assms unfolding sums_def
+ by (auto dest: tendsto_vec_nth [where i=i])
+
+lemma summable_vec_nth :
+ assumes "summable f"
+ shows "summable (\<lambda>x. f x $ i)"
+ using assms unfolding summable_def
+ by (blast intro: sums_vec_nth)
+
lemma closed_eucl_atLeastAtMost[simp, intro]:
fixes a :: "'a::ordered_euclidean_space"
shows "closed {a..b}"
--- a/src/HOL/Analysis/Path_Connected.thy Thu Apr 25 10:19:48 2019 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Fri Apr 26 16:51:40 2019 +0100
@@ -5,7 +5,7 @@
section \<open>Path-Connectedness\<close>
theory Path_Connected
- imports Starlike
+ imports Starlike T1_Spaces
begin
subsection \<open>Paths and Arcs\<close>
@@ -3786,8 +3786,192 @@
apply (rule **) (*such a horrible mess*)
apply (rule connected_Int_frontier [where t = "f`S", OF connected_ball])
using \<open>a \<in> S\<close> \<open>0 < r\<close>
- apply (auto simp: disjoint_iff_not_equal dist_norm)
+ apply (auto simp: disjoint_iff_not_equal dist_norm)
by (metis dw_le norm_minus_commute not_less order_trans rle wy)
qed
+
+subsubsection\<open>Special characterizations of classes of functions into and out of R.\<close>
+
+proposition embedding_map_into_euclideanreal:
+ assumes "path_connected_space X"
+ shows "embedding_map X euclideanreal f \<longleftrightarrow>
+ continuous_map X euclideanreal f \<and> inj_on f (topspace X)"
+ proof safe
+ show "continuous_map X euclideanreal f"
+ if "embedding_map X euclideanreal f"
+ using continuous_map_in_subtopology homeomorphic_imp_continuous_map that
+ unfolding embedding_map_def by blast
+ show "inj_on f (topspace X)"
+ if "embedding_map X euclideanreal f"
+ using that homeomorphic_imp_injective_map
+ unfolding embedding_map_def by blast
+ show "embedding_map X euclideanreal f"
+ if cont: "continuous_map X euclideanreal f" and inj: "inj_on f (topspace X)"
+ proof -
+ obtain g where gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g (f x) = x"
+ using inv_into_f_f [OF inj] by auto
+ show ?thesis
+ unfolding embedding_map_def homeomorphic_map_maps homeomorphic_maps_def
+ proof (intro exI conjI)
+ show "continuous_map X (top_of_set (f ` topspace X)) f"
+ by (simp add: cont continuous_map_in_subtopology)
+ let ?S = "f ` topspace X"
+ have eq: "{x \<in> ?S. g x \<in> U} = f ` U" if "openin X U" for U
+ using openin_subset [OF that] by (auto simp: gf)
+ have 1: "g ` ?S \<subseteq> topspace X"
+ using eq by blast
+ have "openin (top_of_set ?S) {x \<in> ?S. g x \<in> T}"
+ if "openin X T" for T
+ proof -
+ have "T \<subseteq> topspace X"
+ by (simp add: openin_subset that)
+ have RR: "\<forall>x \<in> ?S \<inter> g -` T. \<exists>d>0. \<forall>x' \<in> ?S \<inter> ball x d. g x' \<in> T"
+ proof (clarsimp simp add: gf)
+ have pcS: "path_connectedin euclidean ?S"
+ using assms cont path_connectedin_continuous_map_image path_connectedin_topspace by blast
+ show "\<exists>d>0. \<forall>x'\<in>f ` topspace X \<inter> ball (f x) d. g x' \<in> T"
+ if "x \<in> T" for x
+ proof -
+ have x: "x \<in> topspace X"
+ using \<open>T \<subseteq> topspace X\<close> \<open>x \<in> T\<close> by blast
+ obtain u v d where "0 < d" "u \<in> topspace X" "v \<in> topspace X"
+ and sub_fuv: "?S \<inter> {f x - d .. f x + d} \<subseteq> {f u..f v}"
+ proof (cases "\<exists>u \<in> topspace X. f u < f x")
+ case True
+ then obtain u where u: "u \<in> topspace X" "f u < f x" ..
+ show ?thesis
+ proof (cases "\<exists>v \<in> topspace X. f x < f v")
+ case True
+ then obtain v where v: "v \<in> topspace X" "f x < f v" ..
+ show ?thesis
+ proof
+ let ?d = "min (f x - f u) (f v - f x)"
+ show "0 < ?d"
+ by (simp add: \<open>f u < f x\<close> \<open>f x < f v\<close>)
+ show "f ` topspace X \<inter> {f x - ?d..f x + ?d} \<subseteq> {f u..f v}"
+ by fastforce
+ qed (auto simp: u v)
+ next
+ case False
+ show ?thesis
+ proof
+ let ?d = "f x - f u"
+ show "0 < ?d"
+ by (simp add: u)
+ show "f ` topspace X \<inter> {f x - ?d..f x + ?d} \<subseteq> {f u..f x}"
+ using x u False by auto
+ qed (auto simp: x u)
+ qed
+ next
+ case False
+ note no_u = False
+ show ?thesis
+ proof (cases "\<exists>v \<in> topspace X. f x < f v")
+ case True
+ then obtain v where v: "v \<in> topspace X" "f x < f v" ..
+ show ?thesis
+ proof
+ let ?d = "f v - f x"
+ show "0 < ?d"
+ by (simp add: v)
+ show "f ` topspace X \<inter> {f x - ?d..f x + ?d} \<subseteq> {f x..f v}"
+ using False by auto
+ qed (auto simp: x v)
+ next
+ case False
+ show ?thesis
+ proof
+ show "f ` topspace X \<inter> {f x - 1..f x + 1} \<subseteq> {f x..f x}"
+ using False no_u by fastforce
+ qed (auto simp: x)
+ qed
+ qed
+ then obtain h where "pathin X h" "h 0 = u" "h 1 = v"
+ using assms unfolding path_connected_space_def by blast
+ obtain C where "compactin X C" "connectedin X C" "u \<in> C" "v \<in> C"
+ proof
+ show "compactin X (h ` {0..1})"
+ using that by (simp add: \<open>pathin X h\<close> compactin_path_image)
+ show "connectedin X (h ` {0..1})"
+ using \<open>pathin X h\<close> connectedin_path_image by blast
+ qed (use \<open>h 0 = u\<close> \<open>h 1 = v\<close> in auto)
+ have "continuous_map (subtopology euclideanreal (?S \<inter> {f x - d .. f x + d})) (subtopology X C) g"
+ proof (rule continuous_inverse_map)
+ show "compact_space (subtopology X C)"
+ using \<open>compactin X C\<close> compactin_subspace by blast
+ show "continuous_map (subtopology X C) euclideanreal f"
+ by (simp add: cont continuous_map_from_subtopology)
+ have "{f u .. f v} \<subseteq> f ` topspace (subtopology X C)"
+ proof (rule connected_contains_Icc)
+ show "connected (f ` topspace (subtopology X C))"
+ using connectedin_continuous_map_image [OF cont]
+ by (simp add: \<open>compactin X C\<close> \<open>connectedin X C\<close> compactin_subset_topspace inf_absorb2)
+ show "f u \<in> f ` topspace (subtopology X C)"
+ by (simp add: \<open>u \<in> C\<close> \<open>u \<in> topspace X\<close>)
+ show "f v \<in> f ` topspace (subtopology X C)"
+ by (simp add: \<open>v \<in> C\<close> \<open>v \<in> topspace X\<close>)
+ qed
+ then show "f ` topspace X \<inter> {f x - d..f x + d} \<subseteq> f ` topspace (subtopology X C)"
+ using sub_fuv by blast
+ qed (auto simp: gf)
+ then have contg: "continuous_map (subtopology euclideanreal (?S \<inter> {f x - d .. f x + d})) X g"
+ using continuous_map_in_subtopology by blast
+ have "\<exists>e>0. \<forall>x \<in> ?S \<inter> {f x - d .. f x + d} \<inter> ball (f x) e. g x \<in> T"
+ using openin_continuous_map_preimage [OF contg \<open>openin X T\<close>] x \<open>x \<in> T\<close> \<open>0 < d\<close>
+ unfolding openin_euclidean_subtopology_iff
+ by (force simp: gf dist_commute)
+ then obtain e where "e > 0 \<and> (\<forall>x\<in>f ` topspace X \<inter> {f x - d..f x + d} \<inter> ball (f x) e. g x \<in> T)"
+ by metis
+ with \<open>0 < d\<close> have "min d e > 0" "\<forall>u. u \<in> topspace X \<longrightarrow> \<bar>f x - f u\<bar> < min d e \<longrightarrow> u \<in> T"
+ using dist_real_def gf by force+
+ then show ?thesis
+ by (metis (full_types) Int_iff dist_real_def image_iff mem_ball gf)
+ qed
+ qed
+ then obtain d where d: "\<And>r. r \<in> ?S \<inter> g -` T \<Longrightarrow>
+ d r > 0 \<and> (\<forall>x \<in> ?S \<inter> ball r (d r). g x \<in> T)"
+ by metis
+ show ?thesis
+ unfolding openin_subtopology
+ proof (intro exI conjI)
+ show "{x \<in> ?S. g x \<in> T} = (\<Union>r \<in> ?S \<inter> g -` T. ball r (d r)) \<inter> f ` topspace X"
+ using d by (auto simp: gf)
+ qed auto
+ qed
+ then show "continuous_map (top_of_set ?S) X g"
+ by (simp add: continuous_map_def gf)
+ qed (auto simp: gf)
+ qed
+qed
+
+subsubsection \<open>An injective function into R is a homeomorphism and so an open map.\<close>
+
+lemma injective_into_1d_eq_homeomorphism:
+ fixes f :: "'a::topological_space \<Rightarrow> real"
+ assumes f: "continuous_on S f" and S: "path_connected S"
+ shows "inj_on f S \<longleftrightarrow> (\<exists>g. homeomorphism S (f ` S) f g)"
+proof
+ show "\<exists>g. homeomorphism S (f ` S) f g"
+ if "inj_on f S"
+ proof -
+ have "embedding_map (top_of_set S) euclideanreal f"
+ using that embedding_map_into_euclideanreal [of "top_of_set S" f] assms by auto
+ then show ?thesis
+ by (simp add: embedding_map_def) (metis all_closedin_homeomorphic_image f homeomorphism_injective_closed_map that)
+ qed
+qed (metis homeomorphism_def inj_onI)
+
+lemma injective_into_1d_imp_open_map:
+ fixes f :: "'a::topological_space \<Rightarrow> real"
+ assumes "continuous_on S f" "path_connected S" "inj_on f S" "openin (subtopology euclidean S) T"
+ shows "openin (subtopology euclidean (f ` S)) (f ` T)"
+ using assms homeomorphism_imp_open_map injective_into_1d_eq_homeomorphism by blast
+
+lemma homeomorphism_into_1d:
+ fixes f :: "'a::topological_space \<Rightarrow> real"
+ assumes "path_connected S" "continuous_on S f" "f ` S = T" "inj_on f S"
+ shows "\<exists>g. homeomorphism S T f g"
+ using assms injective_into_1d_eq_homeomorphism by blast
+
end
--- a/src/HOL/Analysis/T1_Spaces.thy Thu Apr 25 10:19:48 2019 +0200
+++ b/src/HOL/Analysis/T1_Spaces.thy Fri Apr 26 16:51:40 2019 +0100
@@ -507,22 +507,22 @@
qed
lemma continuous_imp_closed_map:
- "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f\<rbrakk> \<Longrightarrow> closed_map X Y f"
+ "\<lbrakk>continuous_map X Y f; compact_space X; Hausdorff_space Y\<rbrakk> \<Longrightarrow> closed_map X Y f"
by (meson closed_map_def closedin_compact_space compactin_imp_closedin image_compactin)
lemma continuous_imp_quotient_map:
- "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f; f ` (topspace X) = topspace Y\<rbrakk>
+ "\<lbrakk>continuous_map X Y f; compact_space X; Hausdorff_space Y; f ` (topspace X) = topspace Y\<rbrakk>
\<Longrightarrow> quotient_map X Y f"
by (simp add: continuous_imp_closed_map continuous_closed_imp_quotient_map)
lemma continuous_imp_homeomorphic_map:
- "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f;
+ "\<lbrakk>continuous_map X Y f; compact_space X; Hausdorff_space Y;
f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
\<Longrightarrow> homeomorphic_map X Y f"
by (simp add: continuous_imp_closed_map bijective_closed_imp_homeomorphic_map)
lemma continuous_imp_embedding_map:
- "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f; inj_on f (topspace X)\<rbrakk>
+ "\<lbrakk>continuous_map X Y f; compact_space X; Hausdorff_space Y; inj_on f (topspace X)\<rbrakk>
\<Longrightarrow> embedding_map X Y f"
by (simp add: continuous_imp_closed_map injective_closed_imp_embedding_map)