--- 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)
+ 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)
+ 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)
+ 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)
+ 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)
+ 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)
+ 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)
+ 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)
+ 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)
+ 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)
+ 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)
+ 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)
+ 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)
+ 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)"
by (simp add: continuous_within filterlim_at_split)
+(* 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 (simp add: open_Int)
+ 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