--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Wed Sep 21 16:59:51 2016 +0100
@@ -2794,6 +2794,14 @@
using ANR_imp_absolute_neighbourhood_retract [OF \<open>ANR S\<close> hom]
by (metis clo closed_closedin open_openin subtopology_UNIV)
+corollary neighbourhood_extension_into_ANR:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T" and "ANR T" "closed S"
+ obtains V g where "S \<subseteq> V" "open V" "continuous_on V g"
+ "g ` V \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ using ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf fim]
+ by (metis \<open>closed S\<close> closed_closedin open_openin subtopology_UNIV)
+
lemma absolute_neighbourhood_extensor_imp_ANR:
fixes S :: "'a::euclidean_space set"
assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
@@ -3739,8 +3747,9 @@
apply (rule homeomorphic_closedin_convex [of S])
using aff_dim_le_DIM [of S] apply auto
done
- have "locally path_connected T"
- by (meson ANR_imp_absolute_neighbourhood_retract \<open>S homeomorphic T\<close> \<open>closedin (subtopology euclidean U) T\<close> \<open>convex U\<close> assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected)
+ then have "locally path_connected T"
+ by (meson ANR_imp_absolute_neighbourhood_retract
+ assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected)
then have S: "locally path_connected S"
if "openin (subtopology euclidean U) V" "T retract_of V" "U \<noteq> {}" for V
using \<open>S homeomorphic T\<close> homeomorphic_locally homeomorphic_path_connectedness by blast
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Sep 21 16:59:51 2016 +0100
@@ -5420,10 +5420,6 @@
subsection\<open> General stepping result for derivative formulas.\<close>
-lemma sum_sqs_eq:
- fixes x::"'a::idom" shows "x * x + y * y = x * (y * 2) \<Longrightarrow> y = x"
- by algebra
-
proposition Cauchy_next_derivative:
assumes "continuous_on (path_image \<gamma>) f'"
and leB: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
--- a/src/HOL/Analysis/Conformal_Mappings.thy Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Wed Sep 21 16:59:51 2016 +0100
@@ -1027,7 +1027,7 @@
using polyfun_extremal [where c=c and B="B+1", OF c]
by (auto simp: bounded_pos eventually_at_infinity_pos *)
moreover have "closed {z. (\<Sum>i\<le>n. c i * z ^ i) \<in> K}"
- apply (rule allI continuous_closed_preimage_univ continuous_intros)+
+ apply (intro allI continuous_closed_preimage_univ continuous_intros)
using \<open>compact K\<close> compact_eq_bounded_closed by blast
ultimately show ?thesis
using closed_Int_compact [OF \<open>closed S\<close>] compact_eq_bounded_closed by blast
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Sep 21 16:59:51 2016 +0100
@@ -5554,6 +5554,31 @@
apply auto
done
+text\<open>A non-singleton connected set is perfect (i.e. has no isolated points). \<close>
+lemma connected_imp_perfect:
+ fixes a :: "'a::metric_space"
+ assumes "connected S" "a \<in> S" and S: "\<And>x. S \<noteq> {x}"
+ shows "a islimpt S"
+proof -
+ have False if "a \<in> T" "open T" "\<And>y. \<lbrakk>y \<in> S; y \<in> T\<rbrakk> \<Longrightarrow> y = a" for T
+ proof -
+ obtain e where "e > 0" and e: "cball a e \<subseteq> T"
+ using \<open>open T\<close> \<open>a \<in> T\<close> by (auto simp: open_contains_cball)
+ have "openin (subtopology euclidean S) {a}"
+ unfolding openin_open using that \<open>a \<in> S\<close> by blast
+ moreover have "closedin (subtopology euclidean S) {a}"
+ by (simp add: assms)
+ ultimately show "False"
+ using \<open>connected S\<close> connected_clopen S by blast
+ qed
+ then show ?thesis
+ unfolding islimpt_def by blast
+qed
+
+lemma connected_imp_perfect_aff_dim:
+ "\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S"
+ using aff_dim_sing connected_imp_perfect by blast
+
subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
lemma is_interval_1:
@@ -10406,7 +10431,7 @@
lemma collinear_3_expand:
"collinear{a,b,c} \<longleftrightarrow> a = c \<or> (\<exists>u. b = u *\<^sub>R a + (1 - u) *\<^sub>R c)"
-proof -
+proof -
have "collinear{a,b,c} = collinear{a,c,b}"
by (simp add: insert_commute)
also have "... = collinear {0, a - c, b - c}"
@@ -10418,6 +10443,27 @@
finally show ?thesis .
qed
+lemma collinear_aff_dim: "collinear S \<longleftrightarrow> aff_dim S \<le> 1"
+proof
+ assume "collinear S"
+ then obtain u and v :: "'a" where "aff_dim S \<le> aff_dim {u,v}"
+ by (metis \<open>collinear S\<close> aff_dim_affine_hull aff_dim_subset collinear_affine_hull)
+ then show "aff_dim S \<le> 1"
+ using order_trans by fastforce
+next
+ assume "aff_dim S \<le> 1"
+ then have le1: "aff_dim (affine hull S) \<le> 1"
+ by simp
+ obtain B where "B \<subseteq> S" and B: "\<not> affine_dependent B" "affine hull S = affine hull B"
+ using affine_basis_exists [of S] by auto
+ then have "finite B" "card B \<le> 2"
+ using B le1 by (auto simp: affine_independent_iff_card)
+ then have "collinear B"
+ by (rule collinear_small)
+ then show "collinear S"
+ by (metis \<open>affine hull S = affine hull B\<close> collinear_affine_hull_collinear)
+qed
+
lemma collinear_midpoint: "collinear{a,midpoint a b,b}"
apply (auto simp: collinear_3 collinear_lemma)
apply (drule_tac x="-1" in spec)
@@ -10443,6 +10489,35 @@
ultimately show ?thesis by blast
qed
+lemma between_imp_collinear:
+ fixes x :: "'a :: euclidean_space"
+ assumes "between (a,b) x"
+ shows "collinear {a,x,b}"
+proof (cases "x = a \<or> x = b \<or> a = b")
+ case True with assms show ?thesis
+ by (auto simp: dist_commute)
+next
+ case False with assms show ?thesis
+ apply (auto simp: collinear_3 collinear_lemma between_norm)
+ apply (drule_tac x="-(norm(b - x) / norm(x - a))" in spec)
+ apply (simp add: vector_add_divide_simps eq_vector_fraction_iff real_vector.scale_minus_right [symmetric])
+ done
+qed
+
+lemma midpoint_between:
+ fixes a b :: "'a::euclidean_space"
+ shows "b = midpoint a c \<longleftrightarrow> between (a,c) b \<and> dist a b = dist b c"
+proof (cases "a = c")
+ case True then show ?thesis
+ by (auto simp: dist_commute)
+next
+ case False
+ show ?thesis
+ apply (rule iffI)
+ apply (simp add: between_midpoint(1) dist_midpoint)
+ using False between_imp_collinear midpoint_collinear by blast
+qed
+
lemma collinear_triples:
assumes "a \<noteq> b"
shows "collinear(insert a (insert b S)) \<longleftrightarrow> (\<forall>x \<in> S. collinear{a,b,x})"
@@ -11157,7 +11232,7 @@
using assms unfolding openin_open
by (metis affine_hull_convex_Int_open hull_subset inf.orderE inf_assoc)
-corollary affine_hull_open_in:
+corollary affine_hull_openin:
fixes S :: "'a::real_normed_vector set"
assumes "openin (subtopology euclidean (affine hull T)) S" "S \<noteq> {}"
shows "affine hull S = affine hull T"
@@ -11180,6 +11255,19 @@
shows "\<lbrakk>convex S; open T; S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow> aff_dim(S \<inter> T) = aff_dim S"
using aff_dim_convex_Int_nonempty_interior interior_eq by blast
+lemma affine_hull_Diff:
+ fixes S:: "'a::real_normed_vector set"
+ assumes ope: "openin (subtopology euclidean (affine hull S)) S" and "finite F" "F \<subset> S"
+ shows "affine hull (S - F) = affine hull S"
+proof -
+ have clo: "closedin (subtopology euclidean S) F"
+ using assms finite_imp_closedin by auto
+ moreover have "S - F \<noteq> {}"
+ using assms by auto
+ ultimately show ?thesis
+ by (metis ope closedin_def topspace_euclidean_subtopology affine_hull_openin openin_trans)
+qed
+
lemma affine_hull_halfspace_lt:
fixes a :: "'a::euclidean_space"
shows "affine hull {x. a \<bullet> x < r} = (if a = 0 \<and> r \<le> 0 then {} else UNIV)"
@@ -11963,6 +12051,44 @@
using in_convex_hull_exchange_unique assms apply blast
by (metis hull_mono inf_le1 inf_le2 insert_inter_insert le_inf_iff)
+lemma Int_closed_segment:
+ fixes b :: "'a::euclidean_space"
+ assumes "b \<in> closed_segment a c \<or> ~collinear{a,b,c}"
+ shows "closed_segment a b \<inter> closed_segment b c = {b}"
+proof (cases "c = a")
+ case True
+ then show ?thesis
+ using assms collinear_3_eq_affine_dependent by fastforce
+next
+ case False
+ from assms show ?thesis
+ proof
+ assume "b \<in> closed_segment a c"
+ moreover have "\<not> affine_dependent {a, c}"
+ by (simp add: affine_independent_2)
+ ultimately show ?thesis
+ using False convex_hull_exchange_Int [of "{a,c}" b "{a}" "{c}"]
+ by (simp add: segment_convex_hull insert_commute)
+ next
+ assume ncoll: "\<not> collinear {a, b, c}"
+ have False if "closed_segment a b \<inter> closed_segment b c \<noteq> {b}"
+ proof -
+ have "b \<in> closed_segment a b" and "b \<in> closed_segment b c"
+ by auto
+ with that obtain d where "b \<noteq> d" "d \<in> closed_segment a b" "d \<in> closed_segment b c"
+ by force
+ then have d: "collinear {a, d, b}" "collinear {b, d, c}"
+ by (auto simp: between_mem_segment between_imp_collinear)
+ have "collinear {a, b, c}"
+ apply (rule collinear_3_trans [OF _ _ \<open>b \<noteq> d\<close>])
+ using d by (auto simp: insert_commute)
+ with ncoll show False ..
+ qed
+ then show ?thesis
+ by blast
+ qed
+qed
+
lemma affine_hull_finite_intersection_hyperplanes:
fixes s :: "'a::euclidean_space set"
obtains f where
@@ -12812,6 +12938,7 @@
finally show "aff_dim S \<le> aff_dim (f ` S)" .
qed
+
text\<open>Choosing a subspace of a given dimension\<close>
proposition choose_subspace_of_subspace:
fixes S :: "'n::euclidean_space set"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Sep 21 16:59:51 2016 +0100
@@ -5894,7 +5894,7 @@
assumes "0 < r"
and "\<forall>x. h(g x) = x"
and "\<forall>x. g(h x) = x"
- and "\<forall>x. continuous (at x) g"
+ and contg: "\<And>x. continuous (at x) g"
and "\<forall>u v. \<exists>w z. g ` cbox u v = cbox w z"
and "\<forall>u v. \<exists>w z. h ` cbox u v = cbox w z"
and "\<forall>u v. content(g ` cbox u v) = r * content (cbox u v)"
@@ -5947,7 +5947,7 @@
show "gauge d'"
using d(1)
unfolding gauge_def d'
- using continuous_open_preimage_univ[OF assms(4)]
+ using continuous_open_preimage_univ[OF _ contg]
by auto
fix p
assume as: "p tagged_division_of h ` cbox a b" "d' fine p"
@@ -5985,7 +5985,7 @@
proof -
assume as: "interior k \<inter> interior k' = {}"
have "z \<in> g ` (interior k \<inter> interior k')"
- using interior_image_subset[OF assms(4) inj(1)] z
+ using interior_image_subset[OF \<open>inj g\<close> contg] z
unfolding image_Int[OF inj(1)] by blast
then show False
using as by blast
@@ -6178,20 +6178,13 @@
assumes "(f has_integral i) (cbox a b)"
and "\<forall>k\<in>Basis. m k \<noteq> 0"
shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
- ((1/ \<bar>setprod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
- apply (rule has_integral_twiddle[where f=f])
- unfolding zero_less_abs_iff content_image_stretch_interval
- unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
- using assms
-proof -
- show "\<forall>y::'a. continuous (at y) (\<lambda>x. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k))"
- apply rule
- apply (rule linear_continuous_at)
- unfolding linear_linear
- unfolding linear_iff inner_simps euclidean_eq_iff[where 'a='a]
- apply (auto simp add: field_simps)
- done
-qed auto
+ ((1/ \<bar>setprod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
+apply (rule has_integral_twiddle[where f=f])
+unfolding zero_less_abs_iff content_image_stretch_interval
+unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
+using assms
+by auto
+
lemma integrable_stretch:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -6199,14 +6192,9 @@
and "\<forall>k\<in>Basis. m k \<noteq> 0"
shows "(\<lambda>x::'a. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) integrable_on
((\<lambda>x. \<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k) ` cbox a b)"
- using assms
- unfolding integrable_on_def
- apply -
- apply (erule exE)
- apply (drule has_integral_stretch)
- apply assumption
- apply auto
- done
+ using assms unfolding integrable_on_def
+ by (force dest: has_integral_stretch)
+
subsection \<open>even more special cases.\<close>
--- a/src/HOL/Analysis/Norm_Arith.thy Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Norm_Arith.thy Wed Sep 21 16:59:51 2016 +0100
@@ -8,6 +8,11 @@
imports "~~/src/HOL/Library/Sum_of_Squares"
begin
+(* FIXME: move elsewhere *)
+lemma sum_sqs_eq:
+ fixes x::"'a::idom" shows "x * x + y * y = x * (y * 2) \<Longrightarrow> y = x"
+ by algebra
+
lemma norm_cmul_rule_thm:
fixes x :: "'a::real_normed_vector"
shows "b \<ge> norm x \<Longrightarrow> \<bar>c\<bar> * b \<ge> norm (scaleR c x)"
--- a/src/HOL/Analysis/Path_Connected.thy Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Wed Sep 21 16:59:51 2016 +0100
@@ -4746,19 +4746,17 @@
lemma connected_equivalence_relation:
assumes "connected S"
and etc: "a \<in> S" "b \<in> S"
- and sym: "\<And>x y z. R x y \<Longrightarrow> R y x"
- and trans: "\<And>x y z. R x y \<and> R y z \<Longrightarrow> R x z"
- and opI: "\<And>a. a \<in> S
- \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. R a x)"
+ and sym: "\<And>x y. \<lbrakk>R x y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> R y x"
+ and trans: "\<And>x y z. \<lbrakk>R x y; R y z; x \<in> S; y \<in> S; z \<in> S\<rbrakk> \<Longrightarrow> R x z"
+ and opI: "\<And>a. a \<in> S \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. R a x)"
shows "R a b"
proof -
have "\<And>a b c. \<lbrakk>a \<in> S; b \<in> S; c \<in> S; R a b\<rbrakk> \<Longrightarrow> R a c"
apply (rule connected_induction_simple [OF \<open>connected S\<close>], simp_all)
- by (meson local.sym local.trans opI)
+ by (meson local.sym local.trans opI openin_imp_subset subsetCE)
then show ?thesis by (metis etc opI)
qed
-
lemma locally_constant_imp_constant:
assumes "connected S"
and opI: "\<And>a. a \<in> S
@@ -5270,6 +5268,12 @@
apply (force simp: convex_Int convex_imp_path_connected)
done
+lemma convex_imp_locally_connected:
+ fixes S :: "'a:: real_normed_vector set"
+ shows "convex S \<Longrightarrow> locally connected S"
+ by (simp add: locally_path_connected_imp_locally_connected convex_imp_locally_path_connected)
+
+
subsection\<open>Relations between components and path components\<close>
lemma path_component_eq_connected_component:
@@ -5741,7 +5745,7 @@
done
qed
-lemma isometry_subspaces:
+corollary isometry_subspaces:
fixes S :: "'a::euclidean_space set"
and T :: "'b::euclidean_space set"
assumes S: "subspace S"
@@ -5751,6 +5755,14 @@
using isometries_subspaces [OF assms]
by metis
+corollary isomorphisms_UNIV_UNIV:
+ assumes "DIM('M) = DIM('N)"
+ obtains f::"'M::euclidean_space \<Rightarrow>'N::euclidean_space" and g
+ where "linear f" "linear g"
+ "\<And>x. norm(f x) = norm x" "\<And>y. norm(g y) = norm y"
+ "\<And>x. g(f x) = x" "\<And>y. f(g y) = y"
+ using assms by (auto simp: dim_UNIV intro: isometries_subspaces [of "UNIV::'M set" "UNIV::'N set"])
+
lemma homeomorphic_subspaces:
fixes S :: "'a::euclidean_space set"
and T :: "'b::euclidean_space set"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Sep 21 16:59:51 2016 +0100
@@ -17,6 +17,7 @@
(* FIXME: move elsewhere *)
+
definition (in monoid_add) support_on :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'b set"
where
"support_on s f = {x\<in>s. f x \<noteq> 0}"
@@ -766,6 +767,11 @@
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
by (auto simp add: closedin_closed)
+lemma finite_imp_closedin:
+ fixes S :: "'a::t1_space set"
+ shows "\<lbrakk>finite S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (subtopology euclidean T) S"
+ by (simp add: finite_imp_closed closed_subset)
+
lemma closedin_singleton [simp]:
fixes a :: "'a::t1_space"
shows "closedin (subtopology euclidean U) {a} \<longleftrightarrow> a \<in> U"
@@ -3611,6 +3617,9 @@
unfolding bounded_def by auto
qed
+lemma bounded_closure_image: "bounded (f ` closure S) \<Longrightarrow> bounded (f ` S)"
+ by (simp add: bounded_subset closure_subset image_mono)
+
lemma bounded_cball[simp,intro]: "bounded (cball x e)"
apply (simp add: bounded_def)
apply (rule_tac x=x in exI)
@@ -3749,7 +3758,8 @@
shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)
-text\<open>Some theorems on sups and infs using the notion "bounded".\<close>
+
+subsection\<open>Some theorems on sups and infs using the notion "bounded".\<close>
lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
by (simp add: bounded_iff)
@@ -6122,22 +6132,21 @@
qed
lemma continuous_open_preimage_univ:
- "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
+ "open s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open {x. f x \<in> s}"
using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
lemma continuous_closed_preimage_univ:
- "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s \<Longrightarrow> closed {x. f x \<in> s}"
+ "closed s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed {x. f x \<in> s}"
using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
-lemma continuous_open_vimage: "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open (f -` s)"
+lemma continuous_open_vimage: "open s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` s)"
unfolding vimage_def by (rule continuous_open_preimage_univ)
-lemma continuous_closed_vimage: "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)"
+lemma continuous_closed_vimage: "closed s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` s)"
unfolding vimage_def by (rule continuous_closed_preimage_univ)
lemma interior_image_subset:
- assumes "\<forall>x. continuous (at x) f"
- and "inj f"
+ assumes "inj f" "\<And>x. continuous (at x) f"
shows "interior (f ` s) \<subseteq> f ` (interior s)"
proof
fix x assume "x \<in> interior (f ` s)"
@@ -6145,7 +6154,7 @@
then have "x \<in> f ` s" by auto
then obtain y where y: "y \<in> s" "x = f y" by auto
have "open (vimage f T)"
- using assms(1) \<open>open T\<close> by (rule continuous_open_vimage)
+ using assms \<open>open T\<close> by (metis continuous_open_vimage)
moreover have "y \<in> vimage f T"
using \<open>x = f y\<close> \<open>x \<in> T\<close> by simp
moreover have "vimage f T \<subseteq> s"
@@ -6774,53 +6783,53 @@
by (auto intro!: image_eqI [where f="\<lambda>x. - x"])
lemma open_negations:
- fixes s :: "'a::real_normed_vector set"
- shows "open s \<Longrightarrow> open ((\<lambda>x. - x) ` s)"
- using open_scaling [of "- 1" s] by simp
+ fixes S :: "'a::real_normed_vector set"
+ shows "open S \<Longrightarrow> open ((\<lambda>x. - x) ` S)"
+ using open_scaling [of "- 1" S] by simp
lemma open_translation:
- fixes s :: "'a::real_normed_vector set"
- assumes "open s"
- shows "open((\<lambda>x. a + x) ` s)"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "open S"
+ shows "open((\<lambda>x. a + x) ` S)"
proof -
{
fix x
have "continuous (at x) (\<lambda>x. x - a)"
by (intro continuous_diff continuous_ident continuous_const)
}
- moreover have "{x. x - a \<in> s} = op + a ` s"
+ moreover have "{x. x - a \<in> S} = op + a ` S"
by force
- ultimately show ?thesis using continuous_open_preimage_univ[of "\<lambda>x. x - a" s]
- using assms by auto
+ ultimately show ?thesis
+ by (metis assms continuous_open_vimage vimage_def)
qed
lemma open_affinity:
- fixes s :: "'a::real_normed_vector set"
- assumes "open s" "c \<noteq> 0"
- shows "open ((\<lambda>x. a + c *\<^sub>R x) ` s)"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "open S" "c \<noteq> 0"
+ shows "open ((\<lambda>x. a + c *\<^sub>R x) ` S)"
proof -
have *: "(\<lambda>x. a + c *\<^sub>R x) = (\<lambda>x. a + x) \<circ> (\<lambda>x. c *\<^sub>R x)"
unfolding o_def ..
- have "op + a ` op *\<^sub>R c ` s = (op + a \<circ> op *\<^sub>R c) ` s"
+ have "op + a ` op *\<^sub>R c ` S = (op + a \<circ> op *\<^sub>R c) ` S"
by auto
then show ?thesis
- using assms open_translation[of "op *\<^sub>R c ` s" a]
+ using assms open_translation[of "op *\<^sub>R c ` S" a]
unfolding *
by auto
qed
lemma interior_translation:
- fixes s :: "'a::real_normed_vector set"
- shows "interior ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (interior s)"
+ fixes S :: "'a::real_normed_vector set"
+ shows "interior ((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (interior S)"
proof (rule set_eqI, rule)
fix x
- assume "x \<in> interior (op + a ` s)"
- then obtain e where "e > 0" and e: "ball x e \<subseteq> op + a ` s"
+ assume "x \<in> interior (op + a ` S)"
+ then obtain e where "e > 0" and e: "ball x e \<subseteq> op + a ` S"
unfolding mem_interior by auto
- then have "ball (x - a) e \<subseteq> s"
+ then have "ball (x - a) e \<subseteq> S"
unfolding subset_eq Ball_def mem_ball dist_norm
by (auto simp add: diff_diff_eq)
- then show "x \<in> op + a ` interior s"
+ then show "x \<in> op + a ` interior S"
unfolding image_iff
apply (rule_tac x="x - a" in bexI)
unfolding mem_interior
@@ -6829,27 +6838,27 @@
done
next
fix x
- assume "x \<in> op + a ` interior s"
- then obtain y e where "e > 0" and e: "ball y e \<subseteq> s" and y: "x = a + y"
+ assume "x \<in> op + a ` interior S"
+ then obtain y e where "e > 0" and e: "ball y e \<subseteq> S" and y: "x = a + y"
unfolding image_iff Bex_def mem_interior by auto
{
fix z
have *: "a + y - z = y + a - z" by auto
assume "z \<in> ball x e"
- then have "z - a \<in> s"
+ then have "z - a \<in> S"
using e[unfolded subset_eq, THEN bspec[where x="z - a"]]
unfolding mem_ball dist_norm y group_add_class.diff_diff_eq2 *
by auto
- then have "z \<in> op + a ` s"
+ then have "z \<in> op + a ` S"
unfolding image_iff by (auto intro!: bexI[where x="z - a"])
}
- then have "ball x e \<subseteq> op + a ` s"
+ then have "ball x e \<subseteq> op + a ` S"
unfolding subset_eq by auto
- then show "x \<in> interior (op + a ` s)"
+ then show "x \<in> interior (op + a ` S)"
unfolding mem_interior using \<open>e > 0\<close> by auto
qed
-text \<open>Topological properties of linear functions.\<close>
+subsection \<open>Topological properties of linear functions.\<close>
lemma linear_lim_0:
assumes "bounded_linear f"
@@ -6877,6 +6886,73 @@
"bounded_linear f \<Longrightarrow> continuous_on s f"
using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
+subsubsection\<open>Relating linear images to open/closed/interior/closure.\<close>
+
+proposition open_surjective_linear_image:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
+ assumes "open A" "linear f" "surj f"
+ shows "open(f ` A)"
+unfolding open_dist
+proof clarify
+ fix x
+ assume "x \<in> A"
+ have "bounded (inv f ` Basis)"
+ by (simp add: finite_imp_bounded)
+ with bounded_pos obtain B where "B > 0" and B: "\<And>x. x \<in> inv f ` Basis \<Longrightarrow> norm x \<le> B"
+ by metis
+ obtain e where "e > 0" and e: "\<And>z. dist z x < e \<Longrightarrow> z \<in> A"
+ by (metis open_dist \<open>x \<in> A\<close> \<open>open A\<close>)
+ define \<delta> where "\<delta> \<equiv> e / B / DIM('b)"
+ show "\<exists>e>0. \<forall>y. dist y (f x) < e \<longrightarrow> y \<in> f ` A"
+ proof (intro exI conjI)
+ show "\<delta> > 0"
+ using \<open>e > 0\<close> \<open>B > 0\<close> by (simp add: \<delta>_def divide_simps) (simp add: mult_less_0_iff)
+ have "y \<in> f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y
+ proof -
+ define u where "u \<equiv> y - f x"
+ show ?thesis
+ proof (rule image_eqI)
+ show "y = f (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i))"
+ apply (simp add: linear_add linear_setsum linear.scaleR \<open>linear f\<close> surj_f_inv_f \<open>surj f\<close>)
+ apply (simp add: euclidean_representation u_def)
+ done
+ have "dist (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i)) x \<le> (\<Sum>i\<in>Basis. norm ((u \<bullet> i) *\<^sub>R inv f i))"
+ by (simp add: dist_norm setsum_norm_le)
+ also have "... = (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar> * norm (inv f i))"
+ by (simp add: )
+ also have "... \<le> (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar>) * B"
+ by (simp add: B setsum_distrib_right setsum_mono mult_left_mono)
+ also have "... \<le> DIM('b) * dist y (f x) * B"
+ apply (rule mult_right_mono [OF setsum_bounded_above])
+ using \<open>0 < B\<close> by (auto simp add: Basis_le_norm dist_norm u_def)
+ also have "... < e"
+ by (metis mult.commute mult.left_commute that)
+ finally show "x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i) \<in> A"
+ by (rule e)
+ qed
+ qed
+ then show "\<forall>y. dist y (f x) < \<delta> \<longrightarrow> y \<in> f ` A"
+ using \<open>e > 0\<close> \<open>B > 0\<close>
+ by (auto simp: \<delta>_def divide_simps mult_less_0_iff)
+ qed
+qed
+
+corollary open_bijective_linear_image_eq:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "linear f" "bij f"
+ shows "open(f ` A) \<longleftrightarrow> open A"
+proof
+ assume "open(f ` A)"
+ then have "open(f -` (f ` A))"
+ using assms by (force simp add: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)
+ then show "open A"
+ by (simp add: assms bij_is_inj inj_vimage_image_eq)
+next
+ assume "open A"
+ then show "open(f ` A)"
+ by (simp add: assms bij_is_surj open_surjective_linear_image)
+qed
+
text \<open>Also bilinear functions, in composition form.\<close>
lemma bilinear_continuous_at_compose:
@@ -7957,7 +8033,7 @@
then show "?L \<subseteq> ?R" ..
qed
-lemma bounded_cbox:
+lemma bounded_cbox [simp]:
fixes a :: "'a::euclidean_space"
shows "bounded (cbox a b)"
proof -
@@ -8384,11 +8460,27 @@
(\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
(\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
+lemma homeomorphismI [intro?]:
+ assumes "continuous_on S f" "continuous_on T g"
+ "f ` S \<subseteq> T" "g ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
+ shows "homeomorphism S T f g"
+ using assms by (force simp: homeomorphism_def)
+
lemma homeomorphism_translation:
fixes a :: "'a :: real_normed_vector"
shows "homeomorphism (op + a ` S) S (op + (- a)) (op + a)"
unfolding homeomorphism_def by (auto simp: algebra_simps continuous_intros)
+lemma homeomorphism_ident: "homeomorphism T T (\<lambda>a. a) (\<lambda>a. a)"
+ by (rule homeomorphismI) (auto simp: continuous_on_id)
+
+lemma homeomorphism_compose:
+ assumes "homeomorphism S T f g" "homeomorphism T U h k"
+ shows "homeomorphism S U (h o f) (g o k)"
+ using assms
+ unfolding homeomorphism_def
+ by (intro conjI ballI continuous_on_compose) (auto simp: image_comp [symmetric])
+
lemma homeomorphism_symD: "homeomorphism S t f g \<Longrightarrow> homeomorphism t S g f"
by (simp add: homeomorphism_def)
@@ -8416,47 +8508,12 @@
by blast
lemma homeomorphic_trans [trans]:
- assumes "s homeomorphic t"
- and "t homeomorphic u"
- shows "s homeomorphic u"
-proof -
- 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"
- using assms(1) unfolding homeomorphic_def homeomorphism_def by auto
- obtain f2 g2 where fg2: "\<forall>x\<in>t. g2 (f2 x) = x" "f2 ` t = u" "continuous_on t f2"
- "\<forall>y\<in>u. f2 (g2 y) = y" "g2 ` u = t" "continuous_on u g2"
- using assms(2) unfolding homeomorphic_def homeomorphism_def by auto
- {
- fix x
- assume "x\<in>s"
- then have "(g1 \<circ> g2) ((f2 \<circ> f1) x) = x"
- using fg1(1)[THEN bspec[where x=x]] and fg2(1)[THEN bspec[where x="f1 x"]] and fg1(2)
- by auto
- }
- moreover have "(f2 \<circ> f1) ` s = u"
- using fg1(2) fg2(2) by auto
- moreover have "continuous_on s (f2 \<circ> f1)"
- using continuous_on_compose[OF fg1(3)] and fg2(3) unfolding fg1(2) by auto
- moreover
- {
- fix y
- assume "y\<in>u"
- then have "(f2 \<circ> f1) ((g1 \<circ> g2) y) = y"
- using fg2(4)[THEN bspec[where x=y]] and fg1(4)[THEN bspec[where x="g2 y"]] and fg2(5)
- by auto
- }
- moreover have "(g1 \<circ> g2) ` u = s" using fg1(5) fg2(5) by auto
- moreover have "continuous_on u (g1 \<circ> g2)"
- using continuous_on_compose[OF fg2(6)] and fg1(6)
- unfolding fg2(5)
- by auto
- ultimately show ?thesis
- unfolding homeomorphic_def homeomorphism_def
- apply (rule_tac x="f2 \<circ> f1" in exI)
- apply (rule_tac x="g1 \<circ> g2" in exI)
- apply auto
- done
-qed
+ assumes "S homeomorphic T"
+ and "T homeomorphic U"
+ shows "S homeomorphic U"
+ using assms
+ unfolding homeomorphic_def
+by (metis homeomorphism_compose)
lemma homeomorphic_minimal:
"s homeomorphic t \<longleftrightarrow>
--- a/src/HOL/Library/Disjoint_Sets.thy Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy Wed Sep 21 16:59:51 2016 +0100
@@ -65,6 +65,26 @@
abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV"
+lemma disjoint_family_elem_disjnt:
+ assumes "infinite A" "finite C"
+ and df: "disjoint_family_on B A"
+ obtains x where "x \<in> A" "disjnt C (B x)"
+proof -
+ have "False" if *: "\<forall>x \<in> A. \<exists>y. y \<in> C \<and> y \<in> B x"
+ proof -
+ obtain g where g: "\<forall>x \<in> A. g x \<in> C \<and> g x \<in> B x"
+ using * by metis
+ with df have "inj_on g A"
+ by (fastforce simp add: inj_on_def disjoint_family_on_def)
+ then have "infinite (g ` A)"
+ using \<open>infinite A\<close> finite_image_iff by blast
+ then show False
+ by (meson \<open>finite C\<close> finite_subset g image_subset_iff)
+ qed
+ then show ?thesis
+ by (force simp: disjnt_iff intro: that)
+qed
+
lemma disjoint_family_onD:
"disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
by (auto simp: disjoint_family_on_def)