new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
--- a/src/HOL/Analysis/Abstract_Topology.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Mon Mar 18 15:35:34 2019 +0000
@@ -403,8 +403,12 @@
\<Longrightarrow> closedin (subtopology X (T \<union> U)) S"
by (simp add: closedin_subtopology) blast
-
-subsection \<open>The standard Euclidean topology\<close>
+lemma openin_trans_full:
+ "\<lbrakk>openin (subtopology X U) S; openin X U\<rbrakk> \<Longrightarrow> openin X S"
+ by (simp add: openin_open_subtopology)
+
+
+subsection \<open>The canonical topology from the underlying type class\<close>
abbreviation%important euclidean :: "'a::topological_space topology"
where "euclidean \<equiv> topology open"
@@ -1269,6 +1273,144 @@
by (simp add: Diff_eq discrete_topology_closure_of frontier_of_closures)
+subsection\<open>Locally finite collections\<close>
+
+definition locally_finite_in
+ where
+ "locally_finite_in X \<A> \<longleftrightarrow>
+ (\<Union>\<A> \<subseteq> topspace X) \<and>
+ (\<forall>x \<in> topspace X. \<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> \<A>. U \<inter> V \<noteq> {}})"
+
+lemma finite_imp_locally_finite_in:
+ "\<lbrakk>finite \<A>; \<Union>\<A> \<subseteq> topspace X\<rbrakk> \<Longrightarrow> locally_finite_in X \<A>"
+ by (auto simp: locally_finite_in_def)
+
+lemma locally_finite_in_subset:
+ assumes "locally_finite_in X \<A>" "\<B> \<subseteq> \<A>"
+ shows "locally_finite_in X \<B>"
+proof -
+ have "finite {U \<in> \<A>. U \<inter> V \<noteq> {}} \<Longrightarrow> finite {U \<in> \<B>. U \<inter> V \<noteq> {}}" for V
+ apply (erule rev_finite_subset) using \<open>\<B> \<subseteq> \<A>\<close> by blast
+ then show ?thesis
+ using assms unfolding locally_finite_in_def by (fastforce simp add:)
+qed
+
+lemma locally_finite_in_refinement:
+ assumes \<A>: "locally_finite_in X \<A>" and f: "\<And>S. S \<in> \<A> \<Longrightarrow> f S \<subseteq> S"
+ shows "locally_finite_in X (f ` \<A>)"
+proof -
+ show ?thesis
+ unfolding locally_finite_in_def
+ proof safe
+ fix x
+ assume "x \<in> topspace X"
+ then obtain V where "openin X V" "x \<in> V" "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
+ using \<A> unfolding locally_finite_in_def by blast
+ moreover have "{U \<in> \<A>. f U \<inter> V \<noteq> {}} \<subseteq> {U \<in> \<A>. U \<inter> V \<noteq> {}}" for V
+ using f by blast
+ ultimately have "finite {U \<in> \<A>. f U \<inter> V \<noteq> {}}"
+ using finite_subset by blast
+ moreover have "f ` {U \<in> \<A>. f U \<inter> V \<noteq> {}} = {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
+ by blast
+ ultimately have "finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
+ by (metis (no_types, lifting) finite_imageI)
+ then show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
+ using \<open>openin X V\<close> \<open>x \<in> V\<close> by blast
+ next
+ show "\<And>x xa. \<lbrakk>xa \<in> \<A>; x \<in> f xa\<rbrakk> \<Longrightarrow> x \<in> topspace X"
+ by (meson Sup_upper \<A> f locally_finite_in_def subset_iff)
+ qed
+qed
+
+lemma locally_finite_in_subtopology:
+ assumes \<A>: "locally_finite_in X \<A>" "\<Union>\<A> \<subseteq> S"
+ shows "locally_finite_in (subtopology X S) \<A>"
+ unfolding locally_finite_in_def
+proof safe
+ fix x
+ assume x: "x \<in> topspace (subtopology X S)"
+ then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
+ using \<A> unfolding locally_finite_in_def topspace_subtopology by blast
+ show "\<exists>V. openin (subtopology X S) V \<and> x \<in> V \<and> finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
+ proof (intro exI conjI)
+ show "openin (subtopology X S) (S \<inter> V)"
+ by (simp add: \<open>openin X V\<close> openin_subtopology_Int2)
+ have "{U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}} \<subseteq> {U \<in> \<A>. U \<inter> V \<noteq> {}}"
+ by auto
+ with fin show "finite {U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}}"
+ using finite_subset by auto
+ show "x \<in> S \<inter> V"
+ using x \<open>x \<in> V\<close> by (simp add: topspace_subtopology)
+ qed
+next
+ show "\<And>x A. \<lbrakk>x \<in> A; A \<in> \<A>\<rbrakk> \<Longrightarrow> x \<in> topspace (subtopology X S)"
+ using assms unfolding locally_finite_in_def topspace_subtopology by blast
+qed
+
+
+lemma closedin_locally_finite_Union:
+ assumes clo: "\<And>S. S \<in> \<A> \<Longrightarrow> closedin X S" and \<A>: "locally_finite_in X \<A>"
+ shows "closedin X (\<Union>\<A>)"
+ using \<A> unfolding locally_finite_in_def closedin_def
+proof clarify
+ show "openin X (topspace X - \<Union>\<A>)"
+ proof (subst openin_subopen, clarify)
+ fix x
+ assume "x \<in> topspace X" and "x \<notin> \<Union>\<A>"
+ then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
+ using \<A> unfolding locally_finite_in_def by blast
+ let ?T = "V - \<Union>{S \<in> \<A>. S \<inter> V \<noteq> {}}"
+ show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> topspace X - \<Union>\<A>"
+ proof (intro exI conjI)
+ show "openin X ?T"
+ by (metis (no_types, lifting) fin \<open>openin X V\<close> clo closedin_Union mem_Collect_eq openin_diff)
+ show "x \<in> ?T"
+ using \<open>x \<notin> \<Union>\<A>\<close> \<open>x \<in> V\<close> by auto
+ show "?T \<subseteq> topspace X - \<Union>\<A>"
+ using \<open>openin X V\<close> openin_subset by auto
+ qed
+ qed
+qed
+
+lemma locally_finite_in_closure:
+ assumes \<A>: "locally_finite_in X \<A>"
+ shows "locally_finite_in X ((\<lambda>S. X closure_of S) ` \<A>)"
+ using \<A> unfolding locally_finite_in_def
+proof (intro conjI; clarsimp)
+ fix x A
+ assume "x \<in> X closure_of A"
+ then show "x \<in> topspace X"
+ by (meson in_closure_of)
+next
+ fix x
+ assume "x \<in> topspace X" and "\<Union>\<A> \<subseteq> topspace X"
+ then obtain V where V: "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
+ using \<A> unfolding locally_finite_in_def by blast
+ have eq: "{y \<in> f ` \<A>. Q y} = f ` {x. x \<in> \<A> \<and> Q(f x)}" for f Q
+ by blast
+ have eq2: "{A \<in> \<A>. X closure_of A \<inter> V \<noteq> {}} = {A \<in> \<A>. A \<inter> V \<noteq> {}}"
+ using openin_Int_closure_of_eq_empty V by blast
+ have "finite {U \<in> (closure_of) X ` \<A>. U \<inter> V \<noteq> {}}"
+ by (simp add: eq eq2 fin)
+ with V show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> (closure_of) X ` \<A>. U \<inter> V \<noteq> {}}"
+ by blast
+qed
+
+lemma closedin_Union_locally_finite_closure:
+ "locally_finite_in X \<A> \<Longrightarrow> closedin X (\<Union>((\<lambda>S. X closure_of S) ` \<A>))"
+ by (metis (mono_tags) closedin_closure_of closedin_locally_finite_Union imageE locally_finite_in_closure)
+
+lemma closure_of_Union_subset: "\<Union>((\<lambda>S. X closure_of S) ` \<A>) \<subseteq> X closure_of (\<Union>\<A>)"
+ by clarify (meson Union_upper closure_of_mono subsetD)
+
+lemma closure_of_locally_finite_Union:
+ "locally_finite_in X \<A> \<Longrightarrow> X closure_of (\<Union>\<A>) = \<Union>((\<lambda>S. X closure_of S) ` \<A>)"
+ apply (rule closure_of_unique)
+ apply (simp add: SUP_upper2 Sup_le_iff closure_of_subset locally_finite_in_def)
+ apply (simp add: closedin_Union_locally_finite_closure)
+ by (simp add: Sup_le_iff closure_of_minimal)
+
+
subsection\<open>Continuous maps\<close>
definition continuous_map where
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Mon Mar 18 15:35:34 2019 +0000
@@ -9,6 +9,8 @@
Topology_Euclidean_Space
Operator_Norm
Uniform_Limit
+ Function_Topology
+
begin
lemma onorm_componentwise:
@@ -733,4 +735,86 @@
bounded_linear.uniform_limit[OF bounded_linear_blinfun_apply]
bounded_linear.uniform_limit[OF bounded_linear_blinfun_matrix]
+
+subsection \<open>The strong operator topology on continuous linear operators\<close>
+
+text \<open>Let \<open>'a\<close> and \<open>'b\<close> be two normed real vector spaces. Then the space of linear continuous
+operators from \<open>'a\<close> to \<open>'b\<close> has a canonical norm, and therefore a canonical corresponding topology
+(the type classes instantiation are given in \<^file>\<open>Bounded_Linear_Function.thy\<close>).
+
+However, there is another topology on this space, the strong operator topology, where \<open>T\<^sub>n\<close> tends to
+\<open>T\<close> iff, for all \<open>x\<close> in \<open>'a\<close>, then \<open>T\<^sub>n x\<close> tends to \<open>T x\<close>. This is precisely the product topology
+where the target space is endowed with the norm topology. It is especially useful when \<open>'b\<close> is the set
+of real numbers, since then this topology is compact.
+
+We can not implement it using type classes as there is already a topology, but at least we
+can define it as a topology.
+
+Note that there is yet another (common and useful) topology on operator spaces, the weak operator
+topology, defined analogously using the product topology, but where the target space is given the
+weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
+canonical embedding of a space into its bidual. We do not define it there, although it could also be
+defined analogously.
+\<close>
+
+definition%important strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
+where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
+
+lemma strong_operator_topology_topspace:
+ "topspace strong_operator_topology = UNIV"
+unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
+
+lemma strong_operator_topology_basis:
+ fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"
+ assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
+ shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
+proof -
+ have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
+ by (rule product_topology_basis'[OF assms])
+ moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
+ = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"
+ by auto
+ ultimately show ?thesis
+ unfolding strong_operator_topology_def by (subst openin_pullback_topology) auto
+qed
+
+lemma strong_operator_topology_continuous_evaluation:
+ "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
+proof -
+ have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
+ unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
+ using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
+ then show ?thesis unfolding comp_def by simp
+qed
+
+lemma continuous_on_strong_operator_topo_iff_coordinatewise:
+ "continuous_on_topo T strong_operator_topology f
+ \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
+proof (auto)
+ fix x::"'b"
+ assume "continuous_on_topo T strong_operator_topology f"
+ with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
+ have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
+ by simp
+ then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
+ unfolding comp_def by auto
+next
+ assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
+ have "continuous_on_topo T euclidean (blinfun_apply o f)"
+ unfolding euclidean_product_topology
+ apply (rule continuous_on_topo_coordinatewise_then_product, auto)
+ using * unfolding comp_def by auto
+ show "continuous_on_topo T strong_operator_topology f"
+ unfolding strong_operator_topology_def
+ apply (rule continuous_on_topo_pullback')
+ by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
+qed
+
+lemma strong_operator_topology_weaker_than_euclidean:
+ "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
+ by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
+ auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
+
+
+
end
--- a/src/HOL/Analysis/Cartesian_Space.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Space.thy Mon Mar 18 15:35:34 2019 +0000
@@ -671,7 +671,7 @@
by (metis matrix_transpose_mul rank_mul_le_right rank_transpose)
-subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3\<close>\<close>
+subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3/4\<close>\<close>
lemma exhaust_2:
fixes x :: 2
@@ -699,6 +699,19 @@
lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
by (metis exhaust_3)
+lemma exhaust_4:
+ fixes x :: 4
+ shows "x = 1 \<or> x = 2 \<or> x = 3 \<or> x = 4"
+proof (induct x)
+ case (of_int z)
+ then have "0 \<le> z" and "z < 4" by simp_all
+ then have "z = 0 \<or> z = 1 \<or> z = 2 \<or> z = 3" by arith
+ then show ?case by auto
+qed
+
+lemma forall_4: "(\<forall>i::4. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3 \<and> P 4"
+ by (metis exhaust_4)
+
lemma UNIV_1 [simp]: "UNIV = {1::1}"
by (auto simp add: num1_eq_iff)
@@ -708,6 +721,9 @@
lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
using exhaust_3 by auto
+lemma UNIV_4: "UNIV = {1::4, 2::4, 3::4, 4::4}"
+ using exhaust_4 by auto
+
lemma sum_1: "sum f (UNIV::1 set) = f 1"
unfolding UNIV_1 by simp
@@ -717,6 +733,9 @@
lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
unfolding UNIV_3 by (simp add: ac_simps)
+lemma sum_4: "sum f (UNIV::4 set) = f 1 + f 2 + f 3 + f 4"
+ unfolding UNIV_4 by (simp add: ac_simps)
+
subsection%unimportant\<open>The collapse of the general concepts to dimension one\<close>
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
--- a/src/HOL/Analysis/Continuous_Extension.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Continuous_Extension.thy Mon Mar 18 15:35:34 2019 +0000
@@ -14,7 +14,7 @@
so the "support" must be made explicit in the summation below!\<close>
proposition subordinate_partition_of_unity:
- fixes S :: "'a :: euclidean_space set"
+ fixes S :: "'a::metric_space set"
assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
and fin: "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
obtains F :: "['a set, 'a] \<Rightarrow> real"
@@ -26,9 +26,7 @@
case True
then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
then show ?thesis
- apply (rule_tac F = "\<lambda>V x. if V = W then 1 else 0" in that)
- apply (auto simp: continuous_on_const supp_sum_def support_on_def)
- done
+ by (rule_tac F = "\<lambda>V x. if V = W then 1 else 0" in that) (auto simp: supp_sum_def support_on_def)
next
case False
have nonneg: "0 \<le> supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" for x
@@ -37,9 +35,9 @@
proof -
have "closedin (subtopology euclidean S) (S - V)"
by (simp add: Diff_Diff_Int closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
- with that False setdist_eq_0_closedin [of S "S-V" x] setdist_pos_le [of "{x}" "S - V"]
- show ?thesis
- by (simp add: order_class.order.order_iff_strict)
+ with that False setdist_pos_le [of "{x}" "S - V"]
+ show ?thesis
+ using setdist_gt_0_closedin by fastforce
qed
have ss_pos: "0 < supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" if "x \<in> S" for x
proof -
@@ -50,17 +48,16 @@
then have *: "finite {A \<in> \<C>. \<not> S \<subseteq> A \<and> x \<notin> closure (S - A)}"
using closure_def that by (blast intro: rev_finite_subset)
have "x \<notin> closure (S - U)"
- by (metis \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> less_irrefl sd_pos setdist_eq_0_sing_1 that)
+ using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> opC open_Int_closure_eq_empty by fastforce
then show ?thesis
apply (simp add: setdist_eq_0_sing_1 supp_sum_def support_on_def)
apply (rule ordered_comm_monoid_add_class.sum_pos2 [OF *, of U])
using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> False
- apply (auto simp: setdist_pos_le sd_pos that)
+ apply (auto simp: sd_pos that)
done
qed
define F where
- "F \<equiv> \<lambda>W x. if x \<in> S then setdist {x} (S - W) / supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>
- else 0"
+ "F \<equiv> \<lambda>W x. if x \<in> S then setdist {x} (S - W) / supp_sum (\<lambda>V. setdist {x} (S - V)) \<C> else 0"
show ?thesis
proof (rule_tac F = F in that)
have "continuous_on S (F U)" if "U \<in> \<C>" for U
@@ -302,7 +299,7 @@
text \<open>See \cite{dugundji}.\<close>
theorem Dugundji:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
+ fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
assumes "convex C" "C \<noteq> {}"
and cloin: "closedin (subtopology euclidean U) S"
and contf: "continuous_on S f" and "f ` S \<subseteq> C"
@@ -325,9 +322,8 @@
by (auto simp: sd_pos \<B>_def)
obtain \<C> where USsub: "U - S \<subseteq> \<Union>\<C>"
and nbrhd: "\<And>U. U \<in> \<C> \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<B> \<and> U \<subseteq> T)"
- and fin: "\<And>x. x \<in> U - S
- \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C> \<and> U \<inter> V \<noteq> {}}"
- using paracompact [OF USS] by auto
+ and fin: "\<And>x. x \<in> U - S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C> \<and> U \<inter> V \<noteq> {}}"
+ by (rule paracompact [OF USS]) auto
have "\<exists>v a. v \<in> U \<and> v \<notin> S \<and> a \<in> S \<and>
T \<subseteq> ball v (setdist {v} S / 2) \<and>
dist v a \<le> 2 * setdist {v} S" if "T \<in> \<C>" for T
@@ -353,7 +349,7 @@
proof -
have "dist (\<V> T) v < setdist {\<V> T} S / 2"
using that VA mem_ball by blast
- also have "... \<le> setdist {v} S"
+ also have "\<dots> \<le> setdist {v} S"
using sdle [OF \<open>T \<in> \<C>\<close> \<open>v \<in> T\<close>] by simp
also have vS: "setdist {v} S \<le> dist a v"
by (simp add: setdist_le_dist setdist_sym \<open>a \<in> S\<close>)
@@ -362,9 +358,9 @@
using sdle that vS by force
have "dist a (\<A> T) \<le> dist a v + dist v (\<V> T) + dist (\<V> T) (\<A> T)"
by (metis add.commute add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le)
- also have "... \<le> dist a v + dist a v + dist (\<V> T) (\<A> T)"
+ also have "\<dots> \<le> dist a v + dist a v + dist (\<V> T) (\<A> T)"
using VTV by (simp add: dist_commute)
- also have "... \<le> 2 * dist a v + 2 * setdist {\<V> T} S"
+ also have "\<dots> \<le> 2 * dist a v + 2 * setdist {\<V> T} S"
using VA [OF \<open>T \<in> \<C>\<close>] by auto
finally show ?thesis
using VTS by linarith
@@ -477,66 +473,65 @@
corollary Tietze:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
+ fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
assumes "continuous_on S f"
- and "closedin (subtopology euclidean U) S"
- and "0 \<le> B"
- and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
+ and "closedin (subtopology euclidean U) S"
+ and "0 \<le> B"
+ and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
- "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
- using assms
-by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
+ "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
+ using assms by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
corollary%unimportant Tietze_closed_interval:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::euclidean_space"
assumes "continuous_on S f"
- and "closedin (subtopology euclidean U) S"
- and "cbox a b \<noteq> {}"
- and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
+ and "closedin (subtopology euclidean U) S"
+ and "cbox a b \<noteq> {}"
+ and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
- "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
-apply (rule Dugundji [of "cbox a b" U S f])
-using assms by auto
+ "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
+ apply (rule Dugundji [of "cbox a b" U S f])
+ using assms by auto
corollary%unimportant Tietze_closed_interval_1:
- fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> real"
assumes "continuous_on S f"
- and "closedin (subtopology euclidean U) S"
- and "a \<le> b"
- and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
+ and "closedin (subtopology euclidean U) S"
+ and "a \<le> b"
+ and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
- "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
-apply (rule Dugundji [of "cbox a b" U S f])
-using assms by (auto simp: image_subset_iff)
+ "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
+ apply (rule Dugundji [of "cbox a b" U S f])
+ using assms by (auto simp: image_subset_iff)
corollary%unimportant Tietze_open_interval:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::euclidean_space"
assumes "continuous_on S f"
- and "closedin (subtopology euclidean U) S"
- and "box a b \<noteq> {}"
- and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
+ and "closedin (subtopology euclidean U) S"
+ and "box a b \<noteq> {}"
+ and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
- "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
-apply (rule Dugundji [of "box a b" U S f])
-using assms by auto
+ "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
+ apply (rule Dugundji [of "box a b" U S f])
+ using assms by auto
corollary%unimportant Tietze_open_interval_1:
- fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> real"
assumes "continuous_on S f"
- and "closedin (subtopology euclidean U) S"
- and "a < b"
- and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
+ and "closedin (subtopology euclidean U) S"
+ and "a < b"
+ and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
- "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
-apply (rule Dugundji [of "box a b" U S f])
-using assms by (auto simp: image_subset_iff)
+ "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
+ apply (rule Dugundji [of "box a b" U S f])
+ using assms by (auto simp: image_subset_iff)
corollary%unimportant Tietze_unbounded:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
+ fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
assumes "continuous_on S f"
- and "closedin (subtopology euclidean U) S"
+ and "closedin (subtopology euclidean U) S"
obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-apply (rule Dugundji [of UNIV U S f])
-using assms by auto
+ apply (rule Dugundji [of UNIV U S f])
+ using assms by auto
end
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Mon Mar 18 15:35:34 2019 +0000
@@ -3170,4 +3170,71 @@
lemma setdist_le_sing: "x \<in> S ==> setdist S T \<le> setdist {x} T"
using setdist_subset_left by auto
+lemma infdist_eq_setdist: "infdist x A = setdist {x} A"
+ by (simp add: infdist_def setdist_def Setcompr_eq_image)
+
+lemma setdist_eq_infdist: "setdist A B = (if A = {} then 0 else INF a\<in>A. infdist a B)"
+proof -
+ have "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} = (INF x\<in>A. Inf (dist x ` B))"
+ if "b \<in> B" "a \<in> A" for a b
+ proof (rule order_antisym)
+ have "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> Inf (dist x ` B)"
+ if "b \<in> B" "a \<in> A" "x \<in> A" for x
+ proof -
+ have *: "\<And>b'. b' \<in> B \<Longrightarrow> Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> dist x b'"
+ by (metis (mono_tags, lifting) ex_in_conv setdist_def setdist_le_dist that(3))
+ show ?thesis
+ using that by (subst conditionally_complete_lattice_class.le_cInf_iff) (auto simp: *)+
+ qed
+ then show "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> (INF x\<in>A. Inf (dist x ` B))"
+ using that
+ by (subst conditionally_complete_lattice_class.le_cInf_iff) (auto simp: bdd_below_def)
+ next
+ have *: "\<And>x y. \<lbrakk>b \<in> B; a \<in> A; x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> \<exists>a\<in>A. Inf (dist a ` B) \<le> dist x y"
+ by (meson bdd_below_image_dist cINF_lower)
+ show "(INF x\<in>A. Inf (dist x ` B)) \<le> Inf {dist x y |x y. x \<in> A \<and> y \<in> B}"
+ proof (rule conditionally_complete_lattice_class.cInf_mono)
+ show "bdd_below ((\<lambda>x. Inf (dist x ` B)) ` A)"
+ by (metis (no_types, lifting) bdd_belowI2 ex_in_conv infdist_def infdist_nonneg that(1))
+ qed (use that in \<open>auto simp: *\<close>)
+ qed
+ then show ?thesis
+ by (auto simp: setdist_def infdist_def)
+qed
+
+lemma continuous_on_infdist [continuous_intros]: "continuous_on B (\<lambda>y. infdist y A)"
+ by (simp add: continuous_on_setdist infdist_eq_setdist)
+
+proposition setdist_attains_inf:
+ assumes "compact B" "B \<noteq> {}"
+ obtains y where "y \<in> B" "setdist A B = infdist y A"
+proof (cases "A = {}")
+ case True
+ then show thesis
+ by (metis assms diameter_compact_attained infdist_def setdist_def that)
+next
+ case False
+ obtain y where "y \<in> B" and min: "\<And>y'. y' \<in> B \<Longrightarrow> infdist y A \<le> infdist y' A"
+ using continuous_attains_inf [OF assms continuous_on_infdist] by blast
+ show thesis
+ proof
+ have "setdist A B = (INF y\<in>B. infdist y A)"
+ by (metis \<open>B \<noteq> {}\<close> setdist_eq_infdist setdist_sym)
+ also have "\<dots> = infdist y A"
+ proof (rule order_antisym)
+ show "(INF y\<in>B. infdist y A) \<le> infdist y A"
+ proof (rule cInf_lower)
+ show "infdist y A \<in> (\<lambda>y. infdist y A) ` B"
+ using \<open>y \<in> B\<close> by blast
+ show "bdd_below ((\<lambda>y. infdist y A) ` B)"
+ by (meson bdd_belowI2 infdist_nonneg)
+ qed
+ next
+ show "infdist y A \<le> (INF y\<in>B. infdist y A)"
+ by (simp add: \<open>B \<noteq> {}\<close> cINF_greatest min)
+ qed
+ finally show "setdist A B = infdist y A" .
+ qed (fact \<open>y \<in> B\<close>)
+qed
+
end
\ No newline at end of file
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Mon Mar 18 15:35:34 2019 +0000
@@ -810,6 +810,9 @@
shows "\<not> compact (UNIV::'a set)"
by (simp add: compact_eq_bounded_closed)
+lemma not_compact_space_euclideanreal [simp]: "\<not> compact_space euclideanreal"
+ by (simp add: compact_space_def)
+
text\<open>Representing sets as the union of a chain of compact sets.\<close>
lemma closed_Union_compact_subsets:
fixes S :: "'a::{heine_borel,real_normed_vector} set"
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Mon Mar 18 15:35:34 2019 +0000
@@ -5,7 +5,7 @@
section \<open>Finite Product Measure\<close>
theory Finite_Product_Measure
-imports Binary_Product_Measure
+imports Binary_Product_Measure Function_Topology
begin
lemma PiE_choice: "(\<exists>f\<in>Pi\<^sub>E I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
@@ -1202,4 +1202,142 @@
with E show ?thesis by auto
qed
+
+
+subsection \<open>Measurability\<close>
+
+text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
+generated by open sets in the product, and the product sigma algebra, countably generated by
+products of measurable sets along finitely many coordinates. The second one is defined and studied
+in \<^file>\<open>Finite_Product_Measure.thy\<close>.
+
+These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
+but there is a fundamental difference: open sets are generated by arbitrary unions, not only
+countable ones, so typically many open sets will not be measurable with respect to the product sigma
+algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
+only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
+the factor is countably generated).
+
+In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
+compare it with the product sigma algebra as explained above.
+\<close>
+
+lemma measurable_product_coordinates [measurable (raw)]:
+ "(\<lambda>x. x i) \<in> measurable borel borel"
+by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
+
+lemma measurable_product_then_coordinatewise:
+ fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
+ assumes [measurable]: "f \<in> borel_measurable M"
+ shows "(\<lambda>x. f x i) \<in> borel_measurable M"
+proof -
+ have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
+ unfolding comp_def by auto
+ then show ?thesis by simp
+qed
+
+text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
+of the product sigma algebra that is more similar to the one we used above for the product
+topology.\<close>
+
+lemma sets_PiM_finite:
+ "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
+ {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
+proof
+ have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
+ proof (auto)
+ fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
+ then have *: "X i \<in> sets (M i)" for i by simp
+ define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
+ have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
+ define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
+ have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
+ unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
+ moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
+ unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
+ by (auto simp add: PiE_iff, blast)
+ ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
+ qed
+ then show "sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}
+ \<subseteq> sets (Pi\<^sub>M I M)"
+ by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
+
+ have *: "\<exists>X. {f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X \<and>
+ (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
+ if "i \<in> I" "A \<in> sets (M i)" for i A
+ proof -
+ define X where "X = (\<lambda>j. if j = i then A else space (M j))"
+ have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
+ unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
+ by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
+ moreover have "X j \<in> sets (M j)" for j
+ unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
+ moreover have "finite {j. X j \<noteq> space (M j)}"
+ unfolding X_def by simp
+ ultimately show ?thesis by auto
+ qed
+ show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
+ unfolding sets_PiM_single
+ apply (rule sigma_sets_mono')
+ apply (auto simp add: PiE_iff *)
+ done
+qed
+
+lemma sets_PiM_subset_borel:
+ "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
+proof -
+ have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"
+ proof -
+ define I where "I = {i. X i \<noteq> UNIV}"
+ have "finite I" unfolding I_def using that by simp
+ have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
+ unfolding I_def by auto
+ also have "... \<in> sets borel"
+ using that \<open>finite I\<close> by measurable
+ finally show ?thesis by simp
+ qed
+ then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
+ by auto
+ then show ?thesis unfolding sets_PiM_finite space_borel
+ by (simp add: * sets.sigma_sets_subset')
+qed
+
+proposition sets_PiM_equal_borel:
+ "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
+proof
+ obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
+ "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
+ using product_topology_countable_basis by fast
+ have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
+ proof -
+ obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
+ using K(3)[OF \<open>k \<in> K\<close>] by blast
+ show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
+ qed
+ have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
+ proof -
+ obtain B where "B \<subseteq> K" "U = (\<Union>B)"
+ using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
+ have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
+ moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
+ using \<open>B \<subseteq> K\<close> * that by auto
+ ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
+ qed
+ have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
+ apply (rule sets.sigma_sets_subset') using ** by auto
+ then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
+ unfolding borel_def by auto
+qed (simp add: sets_PiM_subset_borel)
+
+lemma measurable_coordinatewise_then_product:
+ fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
+ assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
+ shows "f \<in> borel_measurable M"
+proof -
+ have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
+ by (rule measurable_PiM_single', auto simp add: assms)
+ then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
+qed
+
+
end
--- a/src/HOL/Analysis/Function_Topology.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy Mon Mar 18 15:35:34 2019 +0000
@@ -3,7 +3,7 @@
*)
theory Function_Topology
-imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure
+imports Topology_Euclidean_Space
begin
@@ -945,24 +945,37 @@
lemma continuous_on_product_coordinates [simp]:
"continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
-unfolding continuous_on_topo_UNIV euclidean_product_topology
-by (rule continuous_on_topo_product_coordinates, simp)
+ unfolding continuous_on_topo_UNIV euclidean_product_topology
+ by (rule continuous_on_topo_product_coordinates, simp)
lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
- assumes "\<And>i. continuous_on UNIV (\<lambda>x. f x i)"
- shows "continuous_on UNIV f"
-using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
-by (rule continuous_on_topo_coordinatewise_then_product, simp)
+ fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
+ assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
+ shows "continuous_on S f"
+ using continuous_on_topo_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclideanreal"]
+ by (metis UNIV_I assms continuous_on_continuous_on_topo euclidean_product_topology)
-lemma continuous_on_product_then_coordinatewise:
+lemma continuous_on_product_then_coordinatewise_UNIV:
assumes "continuous_on UNIV f"
shows "continuous_on UNIV (\<lambda>x. f x i)"
using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
by (rule continuous_on_topo_product_then_coordinatewise(1), simp)
-lemma continuous_on_product_coordinatewise_iff:
- "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
-by (auto intro: continuous_on_product_then_coordinatewise)
+lemma continuous_on_product_then_coordinatewise:
+ assumes "continuous_on S f"
+ shows "continuous_on S (\<lambda>x. f x i)"
+proof -
+ have "continuous_on S ((\<lambda>q. q i) \<circ> f)"
+ by (metis assms continuous_on_compose continuous_on_id
+ continuous_on_product_then_coordinatewise_UNIV continuous_on_subset subset_UNIV)
+ then show ?thesis
+ by auto
+qed
+
+lemma continuous_on_coordinatewise_iff:
+ fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
+ shows "continuous_on (A \<inter> S) f \<longleftrightarrow> (\<forall>i. continuous_on (A \<inter> S) (\<lambda>x. f x i))"
+ by (auto simp: continuous_on_product_then_coordinatewise)
subsubsection%important \<open>Topological countability for product spaces\<close>
@@ -1194,86 +1207,6 @@
using product_topology_countable_basis topological_basis_imp_subbasis by auto
-subsection \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)
-
-text \<open>Let \<open>'a\<close> and \<open>'b\<close> be two normed real vector spaces. Then the space of linear continuous
-operators from \<open>'a\<close> to \<open>'b\<close> has a canonical norm, and therefore a canonical corresponding topology
-(the type classes instantiation are given in \<^file>\<open>Bounded_Linear_Function.thy\<close>).
-
-However, there is another topology on this space, the strong operator topology, where \<open>T\<^sub>n\<close> tends to
-\<open>T\<close> iff, for all \<open>x\<close> in \<open>'a\<close>, then \<open>T\<^sub>n x\<close> tends to \<open>T x\<close>. This is precisely the product topology
-where the target space is endowed with the norm topology. It is especially useful when \<open>'b\<close> is the set
-of real numbers, since then this topology is compact.
-
-We can not implement it using type classes as there is already a topology, but at least we
-can define it as a topology.
-
-Note that there is yet another (common and useful) topology on operator spaces, the weak operator
-topology, defined analogously using the product topology, but where the target space is given the
-weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
-canonical embedding of a space into its bidual. We do not define it there, although it could also be
-defined analogously.
-\<close>
-
-definition%important strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
-where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
-
-lemma strong_operator_topology_topspace:
- "topspace strong_operator_topology = UNIV"
-unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
-
-lemma strong_operator_topology_basis:
- fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"
- assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
- shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
-proof -
- have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
- by (rule product_topology_basis'[OF assms])
- moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
- = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"
- by auto
- ultimately show ?thesis
- unfolding strong_operator_topology_def by (subst openin_pullback_topology) auto
-qed
-
-lemma strong_operator_topology_continuous_evaluation:
- "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
-proof -
- have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
- unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
- using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
- then show ?thesis unfolding comp_def by simp
-qed
-
-lemma continuous_on_strong_operator_topo_iff_coordinatewise:
- "continuous_on_topo T strong_operator_topology f
- \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
-proof (auto)
- fix x::"'b"
- assume "continuous_on_topo T strong_operator_topology f"
- with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
- have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
- by simp
- then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
- unfolding comp_def by auto
-next
- assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
- have "continuous_on_topo T euclidean (blinfun_apply o f)"
- unfolding euclidean_product_topology
- apply (rule continuous_on_topo_coordinatewise_then_product, auto)
- using * unfolding comp_def by auto
- show "continuous_on_topo T strong_operator_topology f"
- unfolding strong_operator_topology_def
- apply (rule continuous_on_topo_pullback')
- by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
-qed
-
-lemma strong_operator_topology_weaker_than_euclidean:
- "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
- by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
- auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
-
-
subsection \<open>Metrics on product spaces\<close>
@@ -1650,142 +1583,4 @@
instance "fun" :: (countable, polish_space) polish_space
by standard
-
-
-
-subsection \<open>Measurability\<close> (*FIX ME move? *)
-
-text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
-generated by open sets in the product, and the product sigma algebra, countably generated by
-products of measurable sets along finitely many coordinates. The second one is defined and studied
-in \<^file>\<open>Finite_Product_Measure.thy\<close>.
-
-These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
-but there is a fundamental difference: open sets are generated by arbitrary unions, not only
-countable ones, so typically many open sets will not be measurable with respect to the product sigma
-algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
-only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
-the factor is countably generated).
-
-In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
-compare it with the product sigma algebra as explained above.
-\<close>
-
-lemma measurable_product_coordinates [measurable (raw)]:
- "(\<lambda>x. x i) \<in> measurable borel borel"
-by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
-
-lemma measurable_product_then_coordinatewise:
- fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
- assumes [measurable]: "f \<in> borel_measurable M"
- shows "(\<lambda>x. f x i) \<in> borel_measurable M"
-proof -
- have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
- unfolding comp_def by auto
- then show ?thesis by simp
-qed
-
-text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
-of the product sigma algebra that is more similar to the one we used above for the product
-topology.\<close>
-
-lemma sets_PiM_finite:
- "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
- {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
-proof
- have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
- proof (auto)
- fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
- then have *: "X i \<in> sets (M i)" for i by simp
- define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
- have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
- define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
- have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
- unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
- moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
- unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
- by (auto simp add: PiE_iff, blast)
- ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
- qed
- then show "sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}
- \<subseteq> sets (Pi\<^sub>M I M)"
- by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
-
- have *: "\<exists>X. {f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X \<and>
- (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
- if "i \<in> I" "A \<in> sets (M i)" for i A
- proof -
- define X where "X = (\<lambda>j. if j = i then A else space (M j))"
- have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
- unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
- by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
- moreover have "X j \<in> sets (M j)" for j
- unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
- moreover have "finite {j. X j \<noteq> space (M j)}"
- unfolding X_def by simp
- ultimately show ?thesis by auto
- qed
- show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
- unfolding sets_PiM_single
- apply (rule sigma_sets_mono')
- apply (auto simp add: PiE_iff *)
- done
-qed
-
-lemma sets_PiM_subset_borel:
- "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
-proof -
- have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"
- proof -
- define I where "I = {i. X i \<noteq> UNIV}"
- have "finite I" unfolding I_def using that by simp
- have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
- unfolding I_def by auto
- also have "... \<in> sets borel"
- using that \<open>finite I\<close> by measurable
- finally show ?thesis by simp
- qed
- then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
- by auto
- then show ?thesis unfolding sets_PiM_finite space_borel
- by (simp add: * sets.sigma_sets_subset')
-qed
-
-proposition sets_PiM_equal_borel:
- "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
-proof
- obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
- "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
- using product_topology_countable_basis by fast
- have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
- proof -
- obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
- using K(3)[OF \<open>k \<in> K\<close>] by blast
- show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
- qed
- have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
- proof -
- obtain B where "B \<subseteq> K" "U = (\<Union>B)"
- using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
- have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
- moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
- using \<open>B \<subseteq> K\<close> * that by auto
- ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
- qed
- have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
- apply (rule sets.sigma_sets_subset') using ** by auto
- then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
- unfolding borel_def by auto
-qed (simp add: sets_PiM_subset_borel)
-
-lemma measurable_coordinatewise_then_product:
- fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
- assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
- shows "f \<in> borel_measurable M"
-proof -
- have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
- by (rule measurable_PiM_single', auto simp add: assms)
- then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
-qed
-
end
--- a/src/HOL/Analysis/Homotopy.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Homotopy.thy Mon Mar 18 15:35:34 2019 +0000
@@ -3652,6 +3652,11 @@
using \<open>S \<subseteq> box a b\<close> by auto
qed
+corollary bounded_path_connected_Compl_real:
+ fixes S :: "real set"
+ assumes "bounded S" "path_connected(- S)" shows "S = {}"
+ by (simp add: assms bounded_connected_Compl_real path_connected_imp_connected)
+
lemma bounded_connected_Compl_1:
fixes S :: "'a::{euclidean_space} set"
assumes "bounded S" and conn: "connected(- S)" and 1: "DIM('a) = 1"
--- a/src/HOL/Analysis/Starlike.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy Mon Mar 18 15:35:34 2019 +0000
@@ -6715,13 +6715,12 @@
subsection\<open>Paracompactness\<close>
proposition paracompact:
- fixes S :: "'a :: euclidean_space set"
+ fixes S :: "'a :: {metric_space,second_countable_topology} set"
assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
and "\<And>U. U \<in> \<C>' \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<C> \<and> U \<subseteq> T)"
and "\<And>x. x \<in> S
- \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and>
- finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
+ \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
proof (cases "S = {}")
case True with that show ?thesis by blast
next
@@ -6737,7 +6736,7 @@
apply (rule_tac x = "ball x e" in exI)
using \<open>T \<in> \<C>\<close>
apply (simp add: closure_minimal)
- done
+ using closed_cball closure_minimal by blast
qed
then obtain F G where Gin: "x \<in> G x" and oG: "open (G x)"
and clos: "closure (G x) \<subseteq> F x" and Fin: "F x \<in> \<C>"
@@ -6802,7 +6801,7 @@
qed
corollary paracompact_closedin:
- fixes S :: "'a :: euclidean_space set"
+ fixes S :: "'a :: {metric_space,second_countable_topology} set"
assumes cin: "closedin (subtopology euclidean U) S"
and oin: "\<And>T. T \<in> \<C> \<Longrightarrow> openin (subtopology euclidean U) T"
and "S \<subseteq> \<Union>\<C>"
@@ -6825,7 +6824,7 @@
obtain \<D> where "U \<subseteq> \<Union>\<D>"
and D1: "\<And>U. U \<in> \<D> \<Longrightarrow> open U \<and> (\<exists>T. T \<in> insert (- K) (F ` \<C>) \<and> U \<subseteq> T)"
and D2: "\<And>x. x \<in> U \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<D>. U \<inter> V \<noteq> {}}"
- using paracompact [OF 1 2] by auto
+ by (blast intro: paracompact [OF 1 2])
let ?C = "{U \<inter> V |V. V \<in> \<D> \<and> (V \<inter> K \<noteq> {})}"
show ?thesis
proof (rule_tac \<C>' = "{U \<inter> V |V. V \<in> \<D> \<and> (V \<inter> K \<noteq> {})}" in that)
@@ -6847,7 +6846,7 @@
qed
corollary%unimportant paracompact_closed:
- fixes S :: "'a :: euclidean_space set"
+ fixes S :: "'a :: {metric_space,second_countable_topology} set"
assumes "closed S"
and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
and "S \<subseteq> \<Union>\<C>"
@@ -6855,7 +6854,7 @@
and "\<And>U. U \<in> \<C>' \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<C> \<and> U \<subseteq> T)"
and "\<And>x. \<exists>V. open V \<and> x \<in> V \<and>
finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
-using paracompact_closedin [of UNIV S \<C>] assms by auto
+ by (rule paracompact_closedin [of UNIV S \<C>]) (auto simp: assms)
subsection%unimportant\<open>Closed-graph characterization of continuity\<close>
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Mar 18 15:35:34 2019 +0000
@@ -2241,24 +2241,22 @@
subsection \<open>Set Distance\<close>
lemma setdist_compact_closed:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
- assumes S: "compact S" and T: "closed T"
- and "S \<noteq> {}" "T \<noteq> {}"
- shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
+ fixes A :: "'a::heine_borel set"
+ assumes A: "compact A" and B: "closed B"
+ and "A \<noteq> {}" "B \<noteq> {}"
+ shows "\<exists>x \<in> A. \<exists>y \<in> B. dist x y = setdist A B"
proof -
- have "(\<Union>x\<in> S. \<Union>y \<in> T. {x - y}) \<noteq> {}"
- using assms by blast
- then have "\<exists>x \<in> S. \<exists>y \<in> T. dist x y \<le> setdist S T"
- apply (rule distance_attains_inf [where a=0, OF compact_closed_differences [OF S T]])
- apply (simp add: dist_norm le_setdist_iff)
- apply blast
- done
- then show ?thesis
- by (blast intro!: antisym [OF _ setdist_le_dist] )
+ obtain x where "x \<in> A" "setdist A B = infdist x B"
+ by (metis A assms(3) setdist_attains_inf setdist_sym)
+ moreover
+ obtain y where"y \<in> B" "infdist x B = dist x y"
+ using B \<open>B \<noteq> {}\<close> infdist_attains_inf by blast
+ ultimately show ?thesis
+ using \<open>x \<in> A\<close> \<open>y \<in> B\<close> by auto
qed
lemma setdist_closed_compact:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
+ fixes S :: "'a::heine_borel set"
assumes S: "closed S" and T: "compact T"
and "S \<noteq> {}" "T \<noteq> {}"
shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
@@ -2266,76 +2264,71 @@
by (metis dist_commute setdist_sym)
lemma setdist_eq_0_compact_closed:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
assumes S: "compact S" and T: "closed T"
shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
- apply (cases "S = {} \<or> T = {}", force)
- using setdist_compact_closed [OF S T]
- apply (force intro: setdist_eq_0I )
- done
+proof (cases "S = {} \<or> T = {}")
+ case True
+ then show ?thesis
+ by force
+next
+ case False
+ then show ?thesis
+ by (metis S T disjoint_iff_not_equal in_closed_iff_infdist_zero setdist_attains_inf setdist_eq_0I setdist_sym)
+qed
corollary setdist_gt_0_compact_closed:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
assumes S: "compact S" and T: "closed T"
shows "setdist S T > 0 \<longleftrightarrow> (S \<noteq> {} \<and> T \<noteq> {} \<and> S \<inter> T = {})"
- using setdist_pos_le [of S T] setdist_eq_0_compact_closed [OF assms]
- by linarith
+ using setdist_pos_le [of S T] setdist_eq_0_compact_closed [OF assms] by linarith
lemma setdist_eq_0_closed_compact:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
assumes S: "closed S" and T: "compact T"
shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
using setdist_eq_0_compact_closed [OF T S]
by (metis Int_commute setdist_sym)
lemma setdist_eq_0_bounded:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
+ fixes S :: "'a::heine_borel set"
assumes "bounded S \<or> bounded T"
- shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> closure S \<inter> closure T \<noteq> {}"
- apply (cases "S = {} \<or> T = {}", force)
- using setdist_eq_0_compact_closed [of "closure S" "closure T"]
- setdist_eq_0_closed_compact [of "closure S" "closure T"] assms
- apply (force simp add: bounded_closure compact_eq_bounded_closed)
- done
+ shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> closure S \<inter> closure T \<noteq> {}"
+proof (cases "S = {} \<or> T = {}")
+ case False
+ then show ?thesis
+ using setdist_eq_0_compact_closed [of "closure S" "closure T"]
+ setdist_eq_0_closed_compact [of "closure S" "closure T"] assms
+ by (force simp: bounded_closure compact_eq_bounded_closed)
+qed force
lemma setdist_eq_0_sing_1:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
- shows "setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
- by (auto simp: setdist_eq_0_bounded)
+ "setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
+ by (metis in_closure_iff_infdist_zero infdist_def infdist_eq_setdist)
lemma setdist_eq_0_sing_2:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
- shows "setdist S {x} = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
- by (auto simp: setdist_eq_0_bounded)
+ "setdist S {x} = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
+ by (metis setdist_eq_0_sing_1 setdist_sym)
lemma setdist_neq_0_sing_1:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
- shows "\<lbrakk>setdist {x} S = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
- by (auto simp: setdist_eq_0_sing_1)
+ "\<lbrakk>setdist {x} S = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
+ by (metis setdist_closure_2 setdist_empty2 setdist_eq_0I singletonI)
lemma setdist_neq_0_sing_2:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
- shows "\<lbrakk>setdist S {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
- by (auto simp: setdist_eq_0_sing_2)
+ "\<lbrakk>setdist S {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
+ by (simp add: setdist_neq_0_sing_1 setdist_sym)
lemma setdist_sing_in_set:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
- shows "x \<in> S \<Longrightarrow> setdist {x} S = 0"
- using closure_subset by (auto simp: setdist_eq_0_sing_1)
+ "x \<in> S \<Longrightarrow> setdist {x} S = 0"
+ by (simp add: setdist_eq_0I)
lemma setdist_eq_0_closed:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
- shows "closed S \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
+ "closed S \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
by (simp add: setdist_eq_0_sing_1)
lemma setdist_eq_0_closedin:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U\<rbrakk>
\<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
lemma setdist_gt_0_closedin:
- fixes S :: "'a::{heine_borel,real_normed_vector} set"
shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U; S \<noteq> {}; x \<notin> S\<rbrakk>
\<Longrightarrow> setdist {x} S > 0"
using less_eq_real_def setdist_eq_0_closedin by fastforce
--- a/src/HOL/Analysis/Winding_Numbers.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Winding_Numbers.thy Mon Mar 18 15:35:34 2019 +0000
@@ -935,11 +935,10 @@
proof -
obtain e where "0 < e" and e: "\<And>t. t \<in> {0..1} \<Longrightarrow> e \<le> norm(exp(p t))"
proof
- have "closed (path_image (exp \<circ> p))"
- by (simp add: assms closed_path_image holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image)
+ have "closed (path_image (exp \<circ> p))"
+ by (simp add: assms closed_path_image holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image)
then show "0 < setdist {0} (path_image (exp \<circ> p))"
- by (metis (mono_tags, lifting) compact_sing exp_not_eq_zero imageE path_image_compose
- path_image_nonempty setdist_eq_0_compact_closed setdist_gt_0_compact_closed setdist_eq_0_closed)
+ by (metis exp_not_eq_zero imageE image_comp infdist_eq_setdist infdist_pos_not_in_closed path_defs(4) path_image_nonempty)
next
fix t::real
assume "t \<in> {0..1}"
--- a/src/HOL/Library/Set_Idioms.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Library/Set_Idioms.thy Mon Mar 18 15:35:34 2019 +0000
@@ -44,6 +44,10 @@
lemma all_intersection_of:
"(\<forall>S. (P intersection_of Q) S \<longrightarrow> R S) \<longleftrightarrow> (\<forall>T. P T \<and> T \<subseteq> Collect Q \<longrightarrow> R(\<Inter>T))"
by (auto simp: intersection_of_def)
+
+lemma intersection_ofE:
+ "\<lbrakk>(P intersection_of Q) S; \<And>T. \<lbrakk>P T; T \<subseteq> Collect Q\<rbrakk> \<Longrightarrow> R(\<Inter>T)\<rbrakk> \<Longrightarrow> R S"
+ by (auto simp: intersection_of_def)
lemma union_of_empty:
"P {} \<Longrightarrow> (P union_of Q) {}"
@@ -319,6 +323,9 @@
lemma all_relative_to: "(\<forall>S. (P relative_to U) S \<longrightarrow> Q S) \<longleftrightarrow> (\<forall>S. P S \<longrightarrow> Q(U \<inter> S))"
by (auto simp: relative_to_def)
+lemma relative_toE: "\<lbrakk>(P relative_to U) S; \<And>S. P S \<Longrightarrow> Q(U \<inter> S)\<rbrakk> \<Longrightarrow> Q S"
+ by (auto simp: relative_to_def)
+
lemma relative_to_inc:
"P S \<Longrightarrow> (P relative_to U) (U \<inter> S)"
by (auto simp: relative_to_def)
--- a/src/HOL/Limits.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Limits.thy Mon Mar 18 15:35:34 2019 +0000
@@ -532,6 +532,9 @@
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))"
unfolding continuous_on_def by (auto intro: tendsto_dist)
+lemma continuous_at_dist: "isCont (dist a) b"
+ using continuous_on_dist [OF continuous_on_const continuous_on_id] continuous_on_eq_continuous_within by blast
+
lemma tendsto_norm [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> norm a) F"
unfolding norm_conv_dist by (intro tendsto_intros)