author hoelzl Wed, 15 Jun 2016 22:19:03 +0200 changeset 63332 f164526d8727 parent 63331 247eac9758dd child 63333 158ab2239496
move open_Collect_eq/less to HOL
```--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Jun 17 09:44:16 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Jun 15 22:19:03 2016 +0200
@@ -1437,7 +1437,7 @@

lemma closed_unit_cube: "closed unit_cube"
unfolding unit_cube_def Collect_ball_eq Collect_conj_eq
-  by (rule closed_INT, auto intro!: closed_Collect_le)
+  by (rule closed_INT, auto intro!: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)

lemma compact_unit_cube: "compact unit_cube" (is "compact ?C")
unfolding compact_eq_seq_compact_metric
@@ -1903,7 +1903,7 @@
proof (rule interiorI)
let ?I = "(\<Inter>i\<in>Basis. {x::'a. 0 < x \<bullet> i} \<inter> {x. x \<bullet> i < 1})"
show "open ?I"
-      by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less)
+      by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner continuous_on_const continuous_on_id)
show "\<Sum>Basis /\<^sub>R 2 \<in> ?I"
by simp
show "?I \<subseteq> unit_cube"```
```--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Jun 17 09:44:16 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Jun 15 22:19:03 2016 +0200
@@ -486,7 +486,7 @@
where "v v* m == (\<chi> j. setsum (\<lambda>i. ((m\$i)\$j) * (v\$i)) (UNIV :: 'm set)) :: 'a^'n"

definition "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
-definition transpose where
+definition transpose where
"(transpose::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A\$j)\$i))"
definition "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A\$i)\$j))"
definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A\$i)\$j))"
@@ -942,7 +942,7 @@
unfolding continuous_on_def by (fast intro: tendsto_vec_nth)

lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x\$i}"
-  by (simp add: Collect_all_eq closed_INT closed_Collect_le)
+  by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)

lemma bounded_component_cart: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x \$ i) ` s)"
unfolding bounded_def
@@ -1091,12 +1091,12 @@
lemma closed_interval_left_cart:
fixes b :: "real^'n"
shows "closed {x::real^'n. \<forall>i. x\$i \<le> b\$i}"
-  by (simp add: Collect_all_eq closed_INT closed_Collect_le)
+  by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)

lemma closed_interval_right_cart:
fixes a::"real^'n"
shows "closed {x::real^'n. \<forall>i. a\$i \<le> x\$i}"
-  by (simp add: Collect_all_eq closed_INT closed_Collect_le)
+  by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)

lemma is_interval_cart:
"is_interval (s::(real^'n) set) \<longleftrightarrow>
@@ -1104,16 +1104,16 @@
by (simp add: is_interval_def Ball_def Basis_vec_def inner_axis imp_ex)

lemma closed_halfspace_component_le_cart: "closed {x::real^'n. x\$i \<le> a}"
+  by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)

lemma closed_halfspace_component_ge_cart: "closed {x::real^'n. x\$i \<ge> a}"
+  by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)

lemma open_halfspace_component_lt_cart: "open {x::real^'n. x\$i < a}"
+  by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component)

lemma open_halfspace_component_gt_cart: "open {x::real^'n. x\$i  > a}"
+  by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component)

lemma Lim_component_le_cart:
fixes f :: "'a \<Rightarrow> real^'n"
@@ -1149,7 +1149,7 @@
proof -
{ fix i::'n
have "closed {x::'a ^ 'n. P i \<longrightarrow> x\$i = 0}"
-      by (cases "P i") (simp_all add: closed_Collect_eq) }
+      by (cases "P i") (simp_all add: closed_Collect_eq continuous_on_const continuous_on_id continuous_on_component) }
thus ?thesis
unfolding Collect_all_eq by (simp add: closed_INT)
qed
@@ -1201,7 +1201,7 @@
shows "(\<chi> i. f (axis i 1)) = (\<Sum>i\<in>Basis. f i *\<^sub>R i)"
unfolding euclidean_eq_iff[where 'a="real^'n"]
by simp (simp add: Basis_vec_def inner_axis)
-
+
lemma const_vector_cart:"((\<chi> i. d)::real^'n) = (\<Sum>i\<in>Basis. d *\<^sub>R i)"
by (rule vector_cart)
```
```--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Jun 17 09:44:16 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Jun 15 22:19:03 2016 +0200
@@ -209,8 +209,8 @@
and closed_halfspace_Im_ge: "closed {z. Im(z) \<ge> b}"
and closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
and closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
-  by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
-            isCont_Im continuous_ident continuous_const)+
+  by (intro open_Collect_less closed_Collect_le closed_Collect_eq continuous_on_Re
+            continuous_on_Im continuous_on_id continuous_on_const)+

lemma closed_complex_Reals: "closed (\<real> :: complex set)"
proof -```
```--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jun 17 09:44:16 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Jun 15 22:19:03 2016 +0200
@@ -10557,16 +10557,16 @@
next
case False
define f where "f \<equiv> \<lambda>x. setdist {x} T - setdist {x} S"
-  have contf: "\<And>x. isCont f x"
-    unfolding f_def by (intro continuous_intros continuous_at_setdist)
+  have contf: "continuous_on UNIV f"
+    unfolding f_def by (intro continuous_intros continuous_on_setdist)
show ?thesis
proof (rule_tac U = "{x. f x > 0}" and V = "{x. f x < 0}" in that)
show "{x. 0 < f x} \<inter> {x. f x < 0} = {}"
by auto
show "open {x. 0 < f x}"
-      by (simp add: open_Collect_less contf)
+      by (simp add: open_Collect_less contf continuous_on_const)
show "open {x. f x < 0}"
-      by (simp add: open_Collect_less contf)
+      by (simp add: open_Collect_less contf continuous_on_const)
show "S \<subseteq> {x. 0 < f x}"
apply (clarsimp simp add: f_def setdist_sing_in_set)
using assms```
```--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jun 17 09:44:16 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jun 15 22:19:03 2016 +0200
@@ -7732,51 +7732,6 @@
using assms unfolding closed_def vimage_Compl [symmetric]
by (rule isCont_open_vimage)

-lemma open_Collect_less:
-  fixes f g :: "'a::t2_space \<Rightarrow> real"
-  assumes f: "\<And>x. isCont f x"
-    and g: "\<And>x. isCont g x"
-  shows "open {x. f x < g x}"
-proof -
-  have "open ((\<lambda>x. g x - f x) -` {0<..})"
-    using isCont_diff [OF g f] open_real_greaterThan
-    by (rule isCont_open_vimage)
-  also have "((\<lambda>x. g x - f x) -` {0<..}) = {x. f x < g x}"
-    by auto
-  finally show ?thesis .
-qed
-
-lemma closed_Collect_le:
-  fixes f g :: "'a::t2_space \<Rightarrow> real"
-  assumes f: "\<And>x. isCont f x"
-    and g: "\<And>x. isCont g x"
-  shows "closed {x. f x \<le> g x}"
-proof -
-  have "closed ((\<lambda>x. g x - f x) -` {0..})"
-    using isCont_diff [OF g f] closed_real_atLeast
-    by (rule isCont_closed_vimage)
-  also have "((\<lambda>x. g x - f x) -` {0..}) = {x. f x \<le> g x}"
-    by auto
-  finally show ?thesis .
-qed
-
-lemma closed_Collect_eq:
-  fixes f g :: "'a::t2_space \<Rightarrow> 'b::t2_space"
-  assumes f: "\<And>x. isCont f x"
-    and g: "\<And>x. isCont g x"
-  shows "closed {x. f x = g x}"
-proof -
-  have "open {(x::'b, y::'b). x \<noteq> y}"
-    unfolding open_prod_def by (auto dest!: hausdorff)
-  then have "closed {(x::'b, y::'b). x = y}"
-    unfolding closed_def split_def Collect_neg_eq .
-  with isCont_Pair [OF f g]
-  have "closed ((\<lambda>x. (f x, g x)) -` {(x, y). x = y})"
-    by (rule isCont_closed_vimage)
-  also have "\<dots> = {x. f x = g x}" by auto
-  finally show ?thesis .
-qed
-
lemma continuous_on_closed_Collect_le:
fixes f g :: "'a::t2_space \<Rightarrow> real"
assumes f: "continuous_on s f" and g: "continuous_on s g" and s: "closed s"
@@ -7794,29 +7749,29 @@
unfolding continuous_at by (intro tendsto_intros)

lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
+  by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)

lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
+  by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)

lemma closed_hyperplane: "closed {x. inner a x = b}"
+  by (simp add: closed_Collect_eq continuous_on_inner continuous_on_const continuous_on_id)

lemma closed_halfspace_component_le: "closed {x::'a::euclidean_space. x\<bullet>i \<le> a}"
+  by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)

lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. x\<bullet>i \<ge> a}"
+  by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)

lemma closed_interval_left:
fixes b :: "'a::euclidean_space"
shows "closed {x::'a. \<forall>i\<in>Basis. x\<bullet>i \<le> b\<bullet>i}"
-  by (simp add: Collect_ball_eq closed_INT closed_Collect_le)
+  by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)

lemma closed_interval_right:
fixes a :: "'a::euclidean_space"
shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
-  by (simp add: Collect_ball_eq closed_INT closed_Collect_le)
+  by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)

lemma continuous_le_on_closure:
fixes a::real
@@ -7840,16 +7795,16 @@
text \<open>Openness of halfspaces.\<close>

lemma open_halfspace_lt: "open {x. inner a x < b}"
+  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)

lemma open_halfspace_gt: "open {x. inner a x > b}"
+  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)

lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. x\<bullet>i < a}"
+  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)

lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\<bullet>i > a}"
+  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)

text \<open>This gives a simple derivation of limit component bounds.\<close>

@@ -8347,7 +8302,7 @@
shows "closed {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i}"
"closed {x. \<forall>i\<in>Basis. x \<bullet> i \<le> a \<bullet> i}"
unfolding eucl_le_eq_halfspaces
-  by (simp_all add: closed_INT closed_Collect_le)
+  by (simp_all add: closed_INT closed_Collect_le  continuous_on_inner continuous_on_const continuous_on_id)

lemma image_affinity_cbox: fixes m::real
fixes a b c :: "'a::euclidean_space"
@@ -9024,7 +8979,7 @@
proof -
let ?D = "{i\<in>Basis. P i}"
have "closed (\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0})"
-    by (simp add: closed_INT closed_Collect_eq)
+    by (simp add: closed_INT closed_Collect_eq continuous_on_inner continuous_on_const continuous_on_id)
also have "(\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0}) = ?A"
by auto
finally show "closed ?A" .```
```--- a/src/HOL/Probability/Borel_Space.thy	Fri Jun 17 09:44:16 2016 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Jun 15 22:19:03 2016 +0200
@@ -15,26 +15,6 @@
"(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
unfolding eventually_sequentially by simp

-lemma open_Collect_less:
-  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
-  assumes "continuous_on UNIV f"
-  assumes "continuous_on UNIV g"
-  shows "open {x. f x < g x}"
-proof -
-  have "open (\<Union>y. {x \<in> UNIV. f x \<in> {..< y}} \<inter> {x \<in> UNIV. g x \<in> {y <..}})" (is "open ?X")
-    by (intro open_UN ballI open_Int continuous_open_preimage assms) auto
-  also have "?X = {x. f x < g x}"
-    by (auto intro: dense)
-  finally show ?thesis .
-qed
-
-lemma closed_Collect_le:
-  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
-  assumes f: "continuous_on UNIV f"
-  assumes g: "continuous_on UNIV g"
-  shows "closed {x. f x \<le> g x}"
-  using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed .
-
lemma topological_basis_trivial: "topological_basis {A. open A}"
by (auto simp: topological_basis_def)

@@ -794,7 +774,7 @@
by (rule borel_measurableI_less) (auto simp: not_le[symmetric])

lemma borel_measurable_less[measurable]:
-  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, linorder_topology}"
assumes "f \<in> borel_measurable M"
assumes "g \<in> borel_measurable M"
shows "{w \<in> space M. f w < g w} \<in> sets M"
@@ -808,7 +788,7 @@
qed

lemma
-  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, linorder_topology}"
assumes f[measurable]: "f \<in> borel_measurable M"
assumes g[measurable]: "g \<in> borel_measurable M"
shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
@@ -947,19 +927,19 @@
unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto

lemma measurable_convergent[measurable (raw)]:
-  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}"
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}"
assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
shows "Measurable.pred M (\<lambda>x. convergent (\<lambda>i. f i x))"
unfolding convergent_ereal by measurable

lemma sets_Collect_convergent[measurable]:
-  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}"
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}"
assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M"
by measurable

lemma borel_measurable_lim[measurable (raw)]:
-  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}"
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}"
assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
proof -
@@ -970,7 +950,7 @@
qed

lemma borel_measurable_LIMSEQ_order:
-  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}"
+  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}"
assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
and u: "\<And>i. u i \<in> borel_measurable M"
shows "u' \<in> borel_measurable M"
@@ -999,7 +979,7 @@
qed simp

lemma borel_measurable_suminf_order[measurable (raw)]:
-  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology, topological_comm_monoid_add}"
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology, topological_comm_monoid_add}"
assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp```
```--- a/src/HOL/Topological_Spaces.thy	Fri Jun 17 09:44:16 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed Jun 15 22:19:03 2016 +0200
@@ -6,7 +6,7 @@
section \<open>Topological Spaces\<close>

theory Topological_Spaces
-imports Main Conditionally_Complete_Lattices
+imports Main
begin

named_theorems continuous_intros "structural introduction rules for continuity"
@@ -1802,6 +1802,58 @@
"continuous (at (x::'a::linorder_topology)) f = (continuous (at_left x) f \<and> continuous (at_right x) f)"

+(* The following open/closed Collect lemmas are ported from Sébastien Gouëzel's Ergodic_Theory *)
+lemma open_Collect_neq:
+  fixes f g :: "'a :: topological_space \<Rightarrow> 'b::t2_space"
+  assumes f: "continuous_on UNIV f" and g: "continuous_on UNIV g"
+  shows "open {x. f x \<noteq> g x}"
+proof (rule openI)
+  fix t assume "t \<in> {x. f x \<noteq> g x}"
+  then obtain U V where *: "open U" "open V" "f t \<in> U" "g t \<in> V" "U \<inter> V = {}"
+    by (auto simp add: separation_t2)
+  with open_vimage[OF \<open>open U\<close> f] open_vimage[OF \<open>open V\<close> g]
+  show "\<exists>T. open T \<and> t \<in> T \<and> T \<subseteq> {x. f x \<noteq> g x}"
+    by (intro exI[of _ "f -` U \<inter> g -` V"]) auto
+qed
+
+lemma closed_Collect_eq:
+  fixes f g :: "'a :: topological_space \<Rightarrow> 'b::t2_space"
+  assumes f: "continuous_on UNIV f" and g: "continuous_on UNIV g"
+  shows "closed {x. f x = g x}"
+  using open_Collect_neq[OF f g] by (simp add: closed_def Collect_neg_eq)
+
+lemma open_Collect_less:
+  fixes f g :: "'a :: topological_space \<Rightarrow> 'b::linorder_topology"
+  assumes f: "continuous_on UNIV f" and g: "continuous_on UNIV g"
+  shows "open {x. f x < g x}"
+proof (rule openI)
+  fix t assume t: "t \<in> {x. f x < g x}"
+  show "\<exists>T. open T \<and> t \<in> T \<and> T \<subseteq> {x. f x < g x}"
+  proof (cases)
+    assume "\<exists>z. f t < z \<and> z < g t"
+    then obtain z where z: "f t < z \<and> z < g t" by blast
+    then show ?thesis
+      using open_vimage[OF _ f, of "{..< z}"] open_vimage[OF _ g, of "{z <..}"]
+      by (intro exI[of _ "f -` {..<z} \<inter> g -` {z<..}"]) auto
+  next
+    assume "\<not>(\<exists>z. f t < z \<and> z < g t)"
+    then have *: "{g t ..} = {f t <..}" "{..< g t} = {.. f t}"
+      using t by (auto intro: leI)
+    show ?thesis
+      using open_vimage[OF _ f, of "{..< g t}"] open_vimage[OF _ g, of "{f t <..}"] t
+      apply (intro exI[of _ "f -` {..< g t} \<inter> g -` {f t<..}"])
+      apply (auto simp add: *)
+      done
+  qed
+qed
+
+lemma closed_Collect_le:
+  fixes f g :: "'a :: topological_space \<Rightarrow> 'b::linorder_topology"
+  assumes f: "continuous_on UNIV f" and g: "continuous_on UNIV g"
+  shows "closed {x. f x \<le> g x}"
+  using open_Collect_less[OF g f] by (simp add: closed_def Collect_neg_eq[symmetric] not_le)
+
subsubsection \<open>Open-cover compactness\<close>

context topological_space```