# HG changeset patch
# User hoelzl
# Date 1466021943 -7200
# Node ID f164526d8727821acb2692cc223dff48cb751d1a
# Parent  247eac9758dd655a0d0652234d0fabc089443ff4
move open_Collect_eq/less to HOL

diff -r 247eac9758dd -r f164526d8727 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- 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"
diff -r 247eac9758dd -r f164526d8727 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- 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)
 
diff -r 247eac9758dd -r f164526d8727 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- 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 -
diff -r 247eac9758dd -r f164526d8727 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- 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
diff -r 247eac9758dd -r f164526d8727 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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" .
diff -r 247eac9758dd -r f164526d8727 src/HOL/Probability/Borel_Space.thy
--- 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
diff -r 247eac9758dd -r f164526d8727 src/HOL/Topological_Spaces.thy
--- 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