2060 by (simp add: norm_sgn) |
2059 by (simp add: norm_sgn) |
2061 then show "\<exists>x::'a. b < norm x" .. |
2060 then show "\<exists>x::'a. b < norm x" .. |
2062 qed |
2061 qed |
2063 |
2062 |
2064 lemma bounded_linear_image: |
2063 lemma bounded_linear_image: |
2065 fixes f :: "real^'m::finite \<Rightarrow> real^'n::finite" |
|
2066 assumes "bounded S" "bounded_linear f" |
2064 assumes "bounded S" "bounded_linear f" |
2067 shows "bounded(f ` S)" |
2065 shows "bounded(f ` S)" |
2068 proof- |
2066 proof- |
2069 from assms(1) obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto |
2067 from assms(1) obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto |
2070 from assms(2) obtain B where B:"B>0" "\<forall>x. norm (f x) \<le> B * norm x" using bounded_linear.pos_bounded by (auto simp add: mult_ac) |
2068 from assms(2) obtain B where B:"B>0" "\<forall>x. norm (f x) \<le> B * norm x" using bounded_linear.pos_bounded by (auto simp add: mult_ac) |
3424 |
3422 |
3425 lemma continuous_const: "continuous net (\<lambda>x. c)" |
3423 lemma continuous_const: "continuous net (\<lambda>x. c)" |
3426 by (auto simp add: continuous_def Lim_const) |
3424 by (auto simp add: continuous_def Lim_const) |
3427 |
3425 |
3428 lemma continuous_cmul: |
3426 lemma continuous_cmul: |
3429 fixes f :: "'a::t2_space \<Rightarrow> real ^ 'n::finite" |
3427 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
3430 shows "continuous net f ==> continuous net (\<lambda>x. c *\<^sub>R f x)" |
3428 shows "continuous net f ==> continuous net (\<lambda>x. c *\<^sub>R f x)" |
3431 by (auto simp add: continuous_def Lim_cmul) |
3429 by (auto simp add: continuous_def Lim_cmul) |
3432 |
3430 |
3433 lemma continuous_neg: |
3431 lemma continuous_neg: |
3434 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
3432 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
3450 lemma continuous_on_const: |
3448 lemma continuous_on_const: |
3451 "continuous_on s (\<lambda>x. c)" |
3449 "continuous_on s (\<lambda>x. c)" |
3452 unfolding continuous_on_eq_continuous_within using continuous_const by blast |
3450 unfolding continuous_on_eq_continuous_within using continuous_const by blast |
3453 |
3451 |
3454 lemma continuous_on_cmul: |
3452 lemma continuous_on_cmul: |
3455 fixes f :: "'a::metric_space \<Rightarrow> real ^ _" |
3453 fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
3456 shows "continuous_on s f ==> continuous_on s (\<lambda>x. c *\<^sub>R (f x))" |
3454 shows "continuous_on s f ==> continuous_on s (\<lambda>x. c *\<^sub>R (f x))" |
3457 unfolding continuous_on_eq_continuous_within using continuous_cmul by blast |
3455 unfolding continuous_on_eq_continuous_within using continuous_cmul by blast |
3458 |
3456 |
3459 lemma continuous_on_neg: |
3457 lemma continuous_on_neg: |
3460 fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
3458 fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
3478 lemma uniformly_continuous_on_const: |
3476 lemma uniformly_continuous_on_const: |
3479 "uniformly_continuous_on s (\<lambda>x. c)" |
3477 "uniformly_continuous_on s (\<lambda>x. c)" |
3480 unfolding uniformly_continuous_on_def by simp |
3478 unfolding uniformly_continuous_on_def by simp |
3481 |
3479 |
3482 lemma uniformly_continuous_on_cmul: |
3480 lemma uniformly_continuous_on_cmul: |
3483 fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _" |
3481 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
|
3482 (* FIXME: generalize 'a to metric_space *) |
3484 assumes "uniformly_continuous_on s f" |
3483 assumes "uniformly_continuous_on s f" |
3485 shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))" |
3484 shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))" |
3486 proof- |
3485 proof- |
3487 { fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially" |
3486 { fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially" |
3488 hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially" |
3487 hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially" |
3867 moreover have "{x. x - a \<in> s} = op + a ` s" apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto |
3866 moreover have "{x. x - a \<in> s} = op + a ` s" apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto |
3868 ultimately show ?thesis using continuous_open_preimage_univ[of "\<lambda>x. x - a" s] using assms by auto |
3867 ultimately show ?thesis using continuous_open_preimage_univ[of "\<lambda>x. x - a" s] using assms by auto |
3869 qed |
3868 qed |
3870 |
3869 |
3871 lemma open_affinity: |
3870 lemma open_affinity: |
3872 fixes s :: "(real ^ _) set" |
3871 fixes s :: "'a::real_normed_vector set" |
3873 assumes "open s" "c \<noteq> 0" |
3872 assumes "open s" "c \<noteq> 0" |
3874 shows "open ((\<lambda>x. a + c *\<^sub>R x) ` s)" |
3873 shows "open ((\<lambda>x. a + c *\<^sub>R x) ` s)" |
3875 proof- |
3874 proof- |
3876 have *:"(\<lambda>x. a + c *\<^sub>R x) = (\<lambda>x. a + x) \<circ> (\<lambda>x. c *\<^sub>R x)" unfolding o_def .. |
3875 have *:"(\<lambda>x. a + c *\<^sub>R x) = (\<lambda>x. a + x) \<circ> (\<lambda>x. c *\<^sub>R x)" unfolding o_def .. |
3877 have "op + a ` op *\<^sub>R c ` s = (op + a \<circ> op *\<^sub>R c) ` s" by auto |
3876 have "op + a ` op *\<^sub>R c ` s = (op + a \<circ> op *\<^sub>R c) ` s" by auto |
4019 thus ?thesis unfolding continuous_on_def by auto |
4018 thus ?thesis unfolding continuous_on_def by auto |
4020 qed |
4019 qed |
4021 |
4020 |
4022 subsection{* Topological properties of linear functions. *} |
4021 subsection{* Topological properties of linear functions. *} |
4023 |
4022 |
4024 lemma linear_lim_0: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite" |
4023 lemma linear_lim_0: |
4025 assumes "bounded_linear f" shows "(f ---> 0) (at (0))" |
4024 assumes "bounded_linear f" shows "(f ---> 0) (at (0))" |
4026 proof- |
4025 proof- |
4027 interpret f: bounded_linear f by fact |
4026 interpret f: bounded_linear f by fact |
4028 have "(f ---> f 0) (at 0)" |
4027 have "(f ---> f 0) (at 0)" |
4029 using tendsto_ident_at by (rule f.tendsto) |
4028 using tendsto_ident_at by (rule f.tendsto) |
4030 thus ?thesis unfolding f.zero . |
4029 thus ?thesis unfolding f.zero . |
4031 qed |
4030 qed |
4032 |
4031 |
4033 lemma bounded_linear_continuous_at: |
4032 lemma linear_continuous_at: |
4034 assumes "bounded_linear f" shows "continuous (at a) f" |
4033 assumes "bounded_linear f" shows "continuous (at a) f" |
4035 unfolding continuous_at using assms |
4034 unfolding continuous_at using assms |
4036 apply (rule bounded_linear.tendsto) |
4035 apply (rule bounded_linear.tendsto) |
4037 apply (rule tendsto_ident_at) |
4036 apply (rule tendsto_ident_at) |
4038 done |
4037 done |
4039 |
4038 |
4040 lemma linear_continuous_at: |
|
4041 fixes f :: "real ^ _ \<Rightarrow> real ^ _" |
|
4042 assumes "bounded_linear f" shows "continuous (at a) f" |
|
4043 using assms by (rule bounded_linear_continuous_at) |
|
4044 |
|
4045 lemma linear_continuous_within: |
4039 lemma linear_continuous_within: |
4046 fixes f :: "real ^ _ \<Rightarrow> real ^ _" |
|
4047 shows "bounded_linear f ==> continuous (at x within s) f" |
4040 shows "bounded_linear f ==> continuous (at x within s) f" |
4048 using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto |
4041 using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto |
4049 |
4042 |
4050 lemma linear_continuous_on: |
4043 lemma linear_continuous_on: |
4051 fixes f :: "real ^ _ \<Rightarrow> real ^ _" |
|
4052 shows "bounded_linear f ==> continuous_on s f" |
4044 shows "bounded_linear f ==> continuous_on s f" |
4053 using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto |
4045 using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto |
4054 |
4046 |
4055 text{* Also bilinear functions, in composition form. *} |
4047 text{* Also bilinear functions, in composition form. *} |
4056 |
4048 |
4057 lemma bilinear_continuous_at_compose: |
4049 lemma bilinear_continuous_at_compose: |
4058 fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _" |
|
4059 shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h |
4050 shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h |
4060 ==> continuous (at x) (\<lambda>x. h (f x) (g x))" |
4051 ==> continuous (at x) (\<lambda>x. h (f x) (g x))" |
4061 unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto |
4052 unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto |
4062 |
4053 |
4063 lemma bilinear_continuous_within_compose: |
4054 lemma bilinear_continuous_within_compose: |
4064 fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _" |
|
4065 shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h |
4055 shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h |
4066 ==> continuous (at x within s) (\<lambda>x. h (f x) (g x))" |
4056 ==> continuous (at x within s) (\<lambda>x. h (f x) (g x))" |
4067 unfolding continuous_within using Lim_bilinear[of f "f x"] by auto |
4057 unfolding continuous_within using Lim_bilinear[of f "f x"] by auto |
4068 |
4058 |
4069 lemma bilinear_continuous_on_compose: |
4059 lemma bilinear_continuous_on_compose: |
4070 fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _" |
|
4071 shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h |
4060 shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h |
4072 ==> continuous_on s (\<lambda>x. h (f x) (g x))" |
4061 ==> continuous_on s (\<lambda>x. h (f x) (g x))" |
4073 unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto |
4062 unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto |
4074 using bilinear_continuous_within_compose[of _ s f g h] by auto |
4063 using bilinear_continuous_within_compose[of _ s f g h] by auto |
4075 |
4064 |
4222 qed |
4211 qed |
4223 |
4212 |
4224 subsection{* We can now extend limit compositions to consider the scalar multiplier. *} |
4213 subsection{* We can now extend limit compositions to consider the scalar multiplier. *} |
4225 |
4214 |
4226 lemma Lim_mul: |
4215 lemma Lim_mul: |
4227 fixes f :: "'a \<Rightarrow> real ^ _" |
4216 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
4228 assumes "(c ---> d) net" "(f ---> l) net" |
4217 assumes "(c ---> d) net" "(f ---> l) net" |
4229 shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net" |
4218 shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net" |
4230 unfolding smult_conv_scaleR using assms by (rule scaleR.tendsto) |
4219 using assms by (rule scaleR.tendsto) |
4231 |
4220 |
4232 lemma Lim_vmul: |
4221 lemma Lim_vmul: |
4233 fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector" |
4222 fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector" |
4234 shows "(c ---> d) net ==> ((\<lambda>x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net" |
4223 shows "(c ---> d) net ==> ((\<lambda>x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net" |
4235 by (intro tendsto_intros) |
4224 by (intro tendsto_intros) |
4356 apply (simp add: o_def) |
4345 apply (simp add: o_def) |
4357 done |
4346 done |
4358 |
4347 |
4359 text{* Hence some useful properties follow quite easily. *} |
4348 text{* Hence some useful properties follow quite easily. *} |
4360 |
4349 |
4361 lemma compact_scaleR_image: |
4350 lemma compact_scaling: |
4362 fixes s :: "'a::real_normed_vector set" |
4351 fixes s :: "'a::real_normed_vector set" |
4363 assumes "compact s" shows "compact ((\<lambda>x. scaleR c x) ` s)" |
4352 assumes "compact s" shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)" |
4364 proof- |
4353 proof- |
4365 let ?f = "\<lambda>x. scaleR c x" |
4354 let ?f = "\<lambda>x. scaleR c x" |
4366 have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right) |
4355 have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right) |
4367 show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f] |
4356 show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f] |
4368 using bounded_linear_continuous_at[OF *] assms by auto |
4357 using linear_continuous_at[OF *] assms by auto |
4369 qed |
4358 qed |
4370 |
|
4371 lemma compact_scaling: |
|
4372 fixes s :: "(real ^ _) set" |
|
4373 assumes "compact s" shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)" |
|
4374 using assms unfolding smult_conv_scaleR by (rule compact_scaleR_image) |
|
4375 |
4359 |
4376 lemma compact_negations: |
4360 lemma compact_negations: |
4377 fixes s :: "'a::real_normed_vector set" |
4361 fixes s :: "'a::real_normed_vector set" |
4378 assumes "compact s" shows "compact ((\<lambda>x. -x) ` s)" |
4362 assumes "compact s" shows "compact ((\<lambda>x. -x) ` s)" |
4379 using compact_scaleR_image [OF assms, of "- 1"] by auto |
4363 using compact_scaling [OF assms, of "- 1"] by auto |
4380 |
4364 |
4381 lemma compact_sums: |
4365 lemma compact_sums: |
4382 fixes s t :: "'a::real_normed_vector set" |
4366 fixes s t :: "'a::real_normed_vector set" |
4383 assumes "compact s" "compact t" shows "compact {x + y | x y. x \<in> s \<and> y \<in> t}" |
4367 assumes "compact s" "compact t" shows "compact {x + y | x y. x \<in> s \<and> y \<in> t}" |
4384 proof- |
4368 proof- |
4405 have "{x + y |x y. x \<in> s \<and> y \<in> {a}} = (\<lambda>x. a + x) ` s" by auto |
4389 have "{x + y |x y. x \<in> s \<and> y \<in> {a}} = (\<lambda>x. a + x) ` s" by auto |
4406 thus ?thesis using compact_sums[OF assms compact_sing[of a]] by auto |
4390 thus ?thesis using compact_sums[OF assms compact_sing[of a]] by auto |
4407 qed |
4391 qed |
4408 |
4392 |
4409 lemma compact_affinity: |
4393 lemma compact_affinity: |
4410 fixes s :: "(real ^ _) set" |
4394 fixes s :: "'a::real_normed_vector set" |
4411 assumes "compact s" shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)" |
4395 assumes "compact s" shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)" |
4412 proof- |
4396 proof- |
4413 have "op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto |
4397 have "op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto |
4414 thus ?thesis using compact_translation[OF compact_scaling[OF assms], of a c] by auto |
4398 thus ?thesis using compact_translation[OF compact_scaling[OF assms], of a c] by auto |
4415 qed |
4399 qed |
4513 unfolding image_iff using `c\<noteq>0` apply(rule_tac x="scaleR (1 / c) l" in bexI) by auto } |
4497 unfolding image_iff using `c\<noteq>0` apply(rule_tac x="scaleR (1 / c) l" in bexI) by auto } |
4514 thus ?thesis unfolding closed_sequential_limits by fast |
4498 thus ?thesis unfolding closed_sequential_limits by fast |
4515 qed |
4499 qed |
4516 qed |
4500 qed |
4517 |
4501 |
4518 lemma closed_scaling: |
|
4519 fixes s :: "(real ^ _) set" |
|
4520 assumes "closed s" shows "closed ((\<lambda>x. c *\<^sub>R x) ` s)" |
|
4521 using assms unfolding smult_conv_scaleR by (rule closed_scaleR_image) |
|
4522 |
|
4523 lemma closed_negations: |
4502 lemma closed_negations: |
4524 fixes s :: "'a::real_normed_vector set" |
4503 fixes s :: "'a::real_normed_vector set" |
4525 assumes "closed s" shows "closed ((\<lambda>x. -x) ` s)" |
4504 assumes "closed s" shows "closed ((\<lambda>x. -x) ` s)" |
4526 using closed_scaleR_image[OF assms, of "- 1"] by simp |
4505 using closed_scaling[OF assms, of "- 1"] by simp |
4527 |
4506 |
4528 lemma compact_closed_sums: |
4507 lemma compact_closed_sums: |
4529 fixes s :: "'a::real_normed_vector set" |
4508 fixes s :: "'a::real_normed_vector set" |
4530 assumes "compact s" "closed t" shows "closed {x + y | x y. x \<in> s \<and> y \<in> t}" |
4509 assumes "compact s" "closed t" shows "closed {x + y | x y. x \<in> s \<and> y \<in> t}" |
4531 proof- |
4510 proof- |
5138 unfolding is_interval_def |
5117 unfolding is_interval_def |
5139 by simp |
5118 by simp |
5140 |
5119 |
5141 subsection{* Closure of halfspaces and hyperplanes. *} |
5120 subsection{* Closure of halfspaces and hyperplanes. *} |
5142 |
5121 |
5143 lemma Lim_dot: fixes f :: "real^'m \<Rightarrow> real^'n::finite" |
5122 lemma Lim_inner: |
5144 assumes "(f ---> l) net" shows "((\<lambda>y. a \<bullet> (f y)) ---> a \<bullet> l) net" |
5123 assumes "(f ---> l) net" shows "((\<lambda>y. inner a (f y)) ---> inner a l) net" |
5145 unfolding dot_def by (intro tendsto_intros assms) |
5124 by (intro tendsto_intros assms) |
5146 |
5125 |
5147 lemma continuous_at_dot: |
5126 lemma continuous_at_inner: "continuous (at x) (inner a)" |
5148 fixes x :: "real ^ _" |
5127 unfolding continuous_at by (intro tendsto_intros) |
5149 shows "continuous (at x) (\<lambda>y. a \<bullet> y)" |
|
5150 proof- |
|
5151 have "((\<lambda>x. x) ---> x) (at x)" unfolding Lim_at by auto |
|
5152 thus ?thesis unfolding continuous_at and o_def using Lim_dot[of "\<lambda>x. x" x "at x" a] by auto |
|
5153 qed |
|
5154 |
|
5155 lemma continuous_on_dot: |
|
5156 fixes s :: "(real ^ _) set" |
|
5157 shows "continuous_on s (\<lambda>y. a \<bullet> y)" |
|
5158 using continuous_at_imp_continuous_on[of s "\<lambda>y. a \<bullet> y"] |
|
5159 using continuous_at_dot |
|
5160 by auto |
|
5161 |
5128 |
5162 lemma continuous_on_inner: |
5129 lemma continuous_on_inner: |
5163 fixes s :: "'a::real_inner set" |
5130 fixes s :: "'a::real_inner set" |
5164 shows "continuous_on s (inner a)" |
5131 shows "continuous_on s (inner a)" |
5165 unfolding continuous_on by (rule ballI) (intro tendsto_intros) |
5132 unfolding continuous_on by (rule ballI) (intro tendsto_intros) |
5264 assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f" |
5231 assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f" |
5265 shows "continuous_on (s \<union> t) f" |
5232 shows "continuous_on (s \<union> t) f" |
5266 using assms unfolding continuous_on unfolding Lim_within_union |
5233 using assms unfolding continuous_on unfolding Lim_within_union |
5267 unfolding Lim unfolding trivial_limit_within unfolding closed_limpt by auto |
5234 unfolding Lim unfolding trivial_limit_within unfolding closed_limpt by auto |
5268 |
5235 |
5269 lemma continuous_on_cases: fixes g :: "real^'m::finite \<Rightarrow> real ^'n::finite" |
5236 lemma continuous_on_cases: |
5270 assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g" |
5237 assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g" |
5271 "\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x" |
5238 "\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x" |
5272 shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)" |
5239 shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)" |
5273 proof- |
5240 proof- |
5274 let ?h = "(\<lambda>x. if P x then f x else g x)" |
5241 let ?h = "(\<lambda>x. if P x then f x else g x)" |
5320 |
5287 |
5321 definition "homeomorphism s t f g \<equiv> |
5288 definition "homeomorphism s t f g \<equiv> |
5322 (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and> |
5289 (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and> |
5323 (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g" |
5290 (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g" |
5324 |
5291 |
5325 definition homeomorphic :: "((real^'a::finite) set) \<Rightarrow> ((real^'b::finite) set) \<Rightarrow> bool" (infixr "homeomorphic" 60) where |
5292 definition |
|
5293 homeomorphic :: "'a::metric_space set \<Rightarrow> 'b::metric_space set \<Rightarrow> bool" |
|
5294 (infixr "homeomorphic" 60) where |
5326 homeomorphic_def: "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)" |
5295 homeomorphic_def: "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)" |
5327 |
5296 |
5328 lemma homeomorphic_refl: "s homeomorphic s" |
5297 lemma homeomorphic_refl: "s homeomorphic s" |
5329 unfolding homeomorphic_def |
5298 unfolding homeomorphic_def |
5330 unfolding homeomorphism_def |
5299 unfolding homeomorphism_def |
5331 using continuous_on_id |
5300 using continuous_on_id |
5332 apply(rule_tac x = "(\<lambda>x::real^'a.x)" in exI) |
5301 apply(rule_tac x = "(\<lambda>x. x)" in exI) |
5333 apply(rule_tac x = "(\<lambda>x::real^'b.x)" in exI) |
5302 apply(rule_tac x = "(\<lambda>x. x)" in exI) |
5334 by blast |
5303 by blast |
5335 |
5304 |
5336 lemma homeomorphic_sym: |
5305 lemma homeomorphic_sym: |
5337 "s homeomorphic t \<longleftrightarrow> t homeomorphic s" |
5306 "s homeomorphic t \<longleftrightarrow> t homeomorphic s" |
5338 unfolding homeomorphic_def |
5307 unfolding homeomorphic_def |
5339 unfolding homeomorphism_def |
5308 unfolding homeomorphism_def |
5340 by blast |
5309 by blast (* FIXME: slow *) |
5341 |
5310 |
5342 lemma homeomorphic_trans: |
5311 lemma homeomorphic_trans: |
5343 assumes "s homeomorphic t" "t homeomorphic u" shows "s homeomorphic u" |
5312 assumes "s homeomorphic t" "t homeomorphic u" shows "s homeomorphic u" |
5344 proof- |
5313 proof- |
5345 obtain f1 g1 where fg1:"\<forall>x\<in>s. g1 (f1 x) = x" "f1 ` s = t" "continuous_on s f1" "\<forall>y\<in>t. f1 (g1 y) = y" "g1 ` t = s" "continuous_on t g1" |
5314 obtain f1 g1 where fg1:"\<forall>x\<in>s. g1 (f1 x) = x" "f1 ` s = t" "continuous_on s f1" "\<forall>y\<in>t. f1 (g1 y) = y" "g1 ` t = s" "continuous_on t g1" |
5377 lemma assumes "inj_on f s" "x\<in>s" |
5346 lemma assumes "inj_on f s" "x\<in>s" |
5378 shows "inv_on f s (f x) = x" |
5347 shows "inv_on f s (f x) = x" |
5379 using assms unfolding inj_on_def inv_on_def by auto |
5348 using assms unfolding inj_on_def inv_on_def by auto |
5380 |
5349 |
5381 lemma homeomorphism_compact: |
5350 lemma homeomorphism_compact: |
5382 fixes f :: "real ^ _ \<Rightarrow> real ^ _" |
5351 fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel" |
|
5352 (* class constraint due to continuous_on_inverse *) |
5383 assumes "compact s" "continuous_on s f" "f ` s = t" "inj_on f s" |
5353 assumes "compact s" "continuous_on s f" "f ` s = t" "inj_on f s" |
5384 shows "\<exists>g. homeomorphism s t f g" |
5354 shows "\<exists>g. homeomorphism s t f g" |
5385 proof- |
5355 proof- |
5386 def g \<equiv> "\<lambda>x. SOME y. y\<in>s \<and> f y = x" |
5356 def g \<equiv> "\<lambda>x. SOME y. y\<in>s \<and> f y = x" |
5387 have g:"\<forall>x\<in>s. g (f x) = x" using assms(3) assms(4)[unfolded inj_on_def] unfolding g_def by auto |
5357 have g:"\<forall>x\<in>s. g (f x) = x" using assms(3) assms(4)[unfolded inj_on_def] unfolding g_def by auto |
5404 show ?thesis unfolding homeomorphism_def homeomorphic_def |
5374 show ?thesis unfolding homeomorphism_def homeomorphic_def |
5405 apply(rule_tac x=g in exI) using g and assms(3) and continuous_on_inverse[OF assms(2,1), of g, unfolded assms(3)] and assms(2) by auto |
5375 apply(rule_tac x=g in exI) using g and assms(3) and continuous_on_inverse[OF assms(2,1), of g, unfolded assms(3)] and assms(2) by auto |
5406 qed |
5376 qed |
5407 |
5377 |
5408 lemma homeomorphic_compact: |
5378 lemma homeomorphic_compact: |
5409 "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s |
5379 fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel" |
|
5380 (* class constraint due to continuous_on_inverse *) |
|
5381 shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s |
5410 \<Longrightarrow> s homeomorphic t" |
5382 \<Longrightarrow> s homeomorphic t" |
5411 unfolding homeomorphic_def by(metis homeomorphism_compact) |
5383 unfolding homeomorphic_def by(metis homeomorphism_compact) |
5412 |
5384 |
5413 text{* Preservation of topological properties. *} |
5385 text{* Preservation of topological properties. *} |
5414 |
5386 |
5418 by (metis compact_continuous_image) |
5390 by (metis compact_continuous_image) |
5419 |
5391 |
5420 text{* Results on translation, scaling etc. *} |
5392 text{* Results on translation, scaling etc. *} |
5421 |
5393 |
5422 lemma homeomorphic_scaling: |
5394 lemma homeomorphic_scaling: |
|
5395 fixes s :: "'a::real_normed_vector set" |
5423 assumes "c \<noteq> 0" shows "s homeomorphic ((\<lambda>x. c *\<^sub>R x) ` s)" |
5396 assumes "c \<noteq> 0" shows "s homeomorphic ((\<lambda>x. c *\<^sub>R x) ` s)" |
5424 unfolding homeomorphic_minimal |
5397 unfolding homeomorphic_minimal |
5425 apply(rule_tac x="\<lambda>x. c *\<^sub>R x" in exI) |
5398 apply(rule_tac x="\<lambda>x. c *\<^sub>R x" in exI) |
5426 apply(rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI) |
5399 apply(rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI) |
5427 using assms apply auto |
5400 using assms apply auto |
5428 using continuous_on_cmul[OF continuous_on_id] by auto |
5401 using continuous_on_cmul[OF continuous_on_id] by auto |
5429 |
5402 |
5430 lemma homeomorphic_translation: |
5403 lemma homeomorphic_translation: |
5431 "s homeomorphic ((\<lambda>x. a + x) ` s)" |
5404 fixes s :: "'a::real_normed_vector set" |
|
5405 shows "s homeomorphic ((\<lambda>x. a + x) ` s)" |
5432 unfolding homeomorphic_minimal |
5406 unfolding homeomorphic_minimal |
5433 apply(rule_tac x="\<lambda>x. a + x" in exI) |
5407 apply(rule_tac x="\<lambda>x. a + x" in exI) |
5434 apply(rule_tac x="\<lambda>x. -a + x" in exI) |
5408 apply(rule_tac x="\<lambda>x. -a + x" in exI) |
5435 using continuous_on_add[OF continuous_on_const continuous_on_id] by auto |
5409 using continuous_on_add[OF continuous_on_const continuous_on_id] by auto |
5436 |
5410 |
5437 lemma homeomorphic_affinity: |
5411 lemma homeomorphic_affinity: |
|
5412 fixes s :: "'a::real_normed_vector set" |
5438 assumes "c \<noteq> 0" shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)" |
5413 assumes "c \<noteq> 0" shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)" |
5439 proof- |
5414 proof- |
5440 have *:"op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto |
5415 have *:"op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto |
5441 show ?thesis |
5416 show ?thesis |
5442 using homeomorphic_trans |
5417 using homeomorphic_trans |
5443 using homeomorphic_scaling[OF assms, of s] |
5418 using homeomorphic_scaling[OF assms, of s] |
5444 using homeomorphic_translation[of "(\<lambda>x. c *\<^sub>R x) ` s" a] unfolding * by auto |
5419 using homeomorphic_translation[of "(\<lambda>x. c *\<^sub>R x) ` s" a] unfolding * by auto |
5445 qed |
5420 qed |
5446 |
5421 |
5447 lemma homeomorphic_balls: fixes a b ::"real^'a::finite" |
5422 lemma homeomorphic_balls: |
|
5423 fixes a b ::"'a::real_normed_vector" (* FIXME: generalize to metric_space *) |
5448 assumes "0 < d" "0 < e" |
5424 assumes "0 < d" "0 < e" |
5449 shows "(ball a d) homeomorphic (ball b e)" (is ?th) |
5425 shows "(ball a d) homeomorphic (ball b e)" (is ?th) |
5450 "(cball a d) homeomorphic (cball b e)" (is ?cth) |
5426 "(cball a d) homeomorphic (cball b e)" (is ?cth) |
5451 proof- |
5427 proof- |
5452 have *:"\<bar>e / d\<bar> > 0" "\<bar>d / e\<bar> >0" using assms using divide_pos_pos by auto |
5428 have *:"\<bar>e / d\<bar> > 0" "\<bar>d / e\<bar> >0" using assms using divide_pos_pos by auto |