# HG changeset patch
# User paulson
# Date 1746461054 -3600
# Node ID 5540532087fa9372066d79b883e34942ae2210d2
# Parent  700f9b01c9d9996fb0434fae6ed689f135d095ca# Parent  5648293625a501bb3c4d524d721d91693a6aa97f
merged

diff -r 700f9b01c9d9 -r 5540532087fa src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Mon May 05 12:42:40 2025 +0200
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Mon May 05 17:04:14 2025 +0100
@@ -1150,37 +1150,50 @@
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic Preserves Topological Properties\<close>
 
 lemma open_scaling[intro]:
-  fixes s :: "'a::real_normed_vector set"
+  fixes S :: "'a::real_normed_vector set"
   assumes "c \<noteq> 0"
-    and "open s"
-  shows "open((\<lambda>x. c *\<^sub>R x) ` s)"
+    and "open S"
+  shows "open((\<lambda>x. c *\<^sub>R x) ` S)"
 proof -
   {
     fix x
-    assume "x \<in> s"
-    then obtain e where "e>0"
-      and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]]
+    assume "x \<in> S"
+    then obtain \<epsilon> where "\<epsilon>>0"
+      and \<epsilon>: "\<forall>x'. dist x' x < \<epsilon> \<longrightarrow> x' \<in> S" using assms(2)[unfolded open_dist, THEN bspec[where x=x]]
       by auto
-    have "e * \<bar>c\<bar> > 0"
-      using assms(1)[unfolded zero_less_abs_iff[symmetric]] \<open>e>0\<close> by auto
+    have "\<epsilon> * \<bar>c\<bar> > 0"
+      using assms(1)[unfolded zero_less_abs_iff[symmetric]] \<open>\<epsilon>>0\<close> by auto
     moreover
     {
       fix y
-      assume "dist y (c *\<^sub>R x) < e * \<bar>c\<bar>"
-      then have "norm (c *\<^sub>R ((1 / c) *\<^sub>R y - x)) < e * norm c"
+      assume "dist y (c *\<^sub>R x) < \<epsilon> * \<bar>c\<bar>"
+      then have "norm (c *\<^sub>R ((1 / c) *\<^sub>R y - x)) < \<epsilon> * norm c"
         by (simp add: \<open>c \<noteq> 0\<close> dist_norm scale_right_diff_distrib)
-      then have "norm ((1 / c) *\<^sub>R y - x) < e"
+      then have "norm ((1 / c) *\<^sub>R y - x) < \<epsilon>"
         by (simp add: \<open>c \<noteq> 0\<close>)
-      then have "y \<in> (*\<^sub>R) c ` s"
-        using rev_image_eqI[of "(1 / c) *\<^sub>R y" s y "(*\<^sub>R) c"]
-        by (simp add: \<open>c \<noteq> 0\<close> dist_norm e)
+      then have "y \<in> (*\<^sub>R) c ` S"
+        using rev_image_eqI[of "(1 / c) *\<^sub>R y" S y "(*\<^sub>R) c"]
+        by (simp add: \<open>c \<noteq> 0\<close> dist_norm \<epsilon>)
     }
-    ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> (*\<^sub>R) c ` s"
-      by (rule_tac x="e * \<bar>c\<bar>" in exI, auto)
+    ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> (*\<^sub>R) c ` S"
+      by (rule_tac x="\<epsilon> * \<bar>c\<bar>" in exI, auto)
   }
   then show ?thesis unfolding open_dist by auto
 qed
 
+lemma open_times_image:
+  fixes S::"'a::real_normed_field set"
+  assumes "c\<noteq>0" "open S"
+  shows "open (((*) c) ` S)" 
+proof -
+  let ?f = "\<lambda>x. x/c" and ?g="((*) c)"
+  have "continuous_on UNIV ?f" using \<open>c\<noteq>0\<close> by (auto intro:continuous_intros)
+  then have "open (?f -` S)" using \<open>open S\<close> by (auto elim:open_vimage)
+  moreover have "?g ` S = ?f -` S" using \<open>c\<noteq>0\<close>
+    using image_iff by fastforce
+  ultimately show ?thesis by auto
+qed   
+
 lemma minus_image_eq_vimage:
   fixes A :: "'a::ab_group_add set"
   shows "(\<lambda>x. - x) ` A = (\<lambda>x. - x) -` A"
diff -r 700f9b01c9d9 -r 5540532087fa src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Mon May 05 12:42:40 2025 +0200
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Mon May 05 17:04:14 2025 +0100
@@ -40,7 +40,27 @@
 
 lemma real_eq_affinity: "m \<noteq> 0 \<Longrightarrow> y = m * x + c  \<longleftrightarrow> inverse m * y + - (c / m) = x"
   for m :: "'a::linordered_field"
-  by (simp add: field_simps)
+  by (metis real_affinity_eq)
+
+lemma image_linear_greaterThan:
+  fixes x::"'a::linordered_field"
+  assumes "c\<noteq>0"
+  shows "((\<lambda>x. c*x+b) ` {x<..}) = (if c>0 then {c*x+b <..} else {..< c*x+b})"
+using  \<open>c\<noteq>0\<close>
+  apply (auto simp add:image_iff field_simps)    
+  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
+  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
+done
+
+lemma image_linear_lessThan:
+  fixes x::"'a::linordered_field"
+  assumes "c\<noteq>0"
+  shows "((\<lambda>x. c*x+b) ` {..<x}) = (if c>0 then {..<c*x+b} else {c*x+b<..})"
+using \<open>c\<noteq>0\<close>
+  apply (auto simp add:image_iff field_simps)    
+  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
+  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
+done
 
 
 subsection \<open>Topological Basis\<close>
@@ -2113,26 +2133,6 @@
       \<longrightarrow> ((f \<circ> x) \<longlongrightarrow> f a) sequentially)"
   by (meson continuous_on_eq_continuous_within continuous_within_sequentially)
 
-text \<open>Continuity in terms of open preimages.\<close>
-
-lemma continuous_at_open:
-  "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t \<longrightarrow> (\<exists>S. open S \<and> x \<in> S \<and> (\<forall>x' \<in> S. (f x') \<in> t)))"
-  by (metis UNIV_I continuous_within_topological)
-
-lemma continuous_imp_tendsto:
-  assumes "continuous (at x0) f" and "x \<longlonglongrightarrow> x0"
-  shows "(f \<circ> x) \<longlonglongrightarrow> (f x0)"
-proof (rule topological_tendstoI)
-  fix S
-  assume "open S" "f x0 \<in> S"
-  then obtain T where T_def: "open T" "x0 \<in> T" "\<forall>x\<in>T. f x \<in> S"
-     using assms continuous_at_open by metis
-  then have "eventually (\<lambda>n. x n \<in> T) sequentially"
-    using assms T_def by (auto simp: tendsto_def)
-  then show "eventually (\<lambda>n. (f \<circ> x) n \<in> S) sequentially"
-    using T_def by (auto elim!: eventually_mono)
-qed
-
 subsection \<open>Homeomorphisms\<close>
 
 definition\<^marker>\<open>tag important\<close> "homeomorphism S T f g \<longleftrightarrow>
diff -r 700f9b01c9d9 -r 5540532087fa src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Mon May 05 12:42:40 2025 +0200
+++ b/src/HOL/Filter.thy	Mon May 05 17:04:14 2025 +0100
@@ -884,6 +884,12 @@
   unfolding at_bot_def
   by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
 
+lemma eventually_at_bot_linorderI:
+  fixes c::"'a::linorder"
+  assumes "\<And>x. x \<le> c \<Longrightarrow> P x"
+  shows "eventually P at_bot"
+  using assms by (auto simp: eventually_at_bot_linorder)     
+
 lemma eventually_filtercomap_at_bot_linorder: 
   "eventually P (filtercomap f at_bot) \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>x. f x \<le> N \<longrightarrow> P x)"
   by (auto simp: eventually_filtercomap eventually_at_bot_linorder)
diff -r 700f9b01c9d9 -r 5540532087fa src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon May 05 12:42:40 2025 +0200
+++ b/src/HOL/Limits.thy	Mon May 05 17:04:14 2025 +0100
@@ -26,6 +26,12 @@
   by (subst eventually_INF_base)
      (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b])
 
+lemma eventually_at_infinityI:
+  fixes P::"'a::real_normed_vector \<Rightarrow> bool"
+  assumes "\<And>x. c \<le> norm x \<Longrightarrow> P x"
+  shows "eventually P at_infinity"  
+unfolding eventually_at_infinity using assms by auto
+
 corollary eventually_at_infinity_pos:
   "eventually p at_infinity \<longleftrightarrow> (\<exists>b. 0 < b \<and> (\<forall>x. norm x \<ge> b \<longrightarrow> p x))"
   unfolding eventually_at_infinity
@@ -1550,7 +1556,34 @@
   for a :: real
   by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
 
-
+lemma filtermap_linear_at_within:
+  assumes "bij f" and cont: "isCont f a" and open_map: "\<And>S. open S \<Longrightarrow> open (f`S)"
+  shows "filtermap f (at a within S) = at (f a) within f`S"
+  unfolding filter_eq_iff
+proof safe
+  fix P
+  assume "eventually P (filtermap f (at a within S))"
+  then obtain T where "open T" "a \<in> T" and impP:"\<forall>x\<in>T. x\<noteq>a \<longrightarrow> x\<in>S\<longrightarrow> P (f x)"
+    by (auto simp: eventually_filtermap eventually_at_topological)
+  then show "eventually P (at (f a) within f ` S)"
+    unfolding eventually_at_topological
+    apply (intro exI[of _ "f`T"])
+    using \<open>bij f\<close> open_map by (metis bij_pointE image_iff)  
+next
+  fix P
+  assume "eventually P (at (f a) within f ` S)"
+  then obtain T1 where "open T1" "f a \<in> T1" and impP:"\<forall>x\<in>T1. x\<noteq>f a \<longrightarrow> x\<in>f`S\<longrightarrow> P (x)"
+    unfolding eventually_at_topological by auto
+  then obtain T2 where "open T2" "a \<in> T2" "(\<forall>x'\<in>T2. f x' \<in> T1)"
+    using cont[unfolded continuous_at_open,rule_format,of T1] by blast 
+  then have "\<forall>x\<in>T2. x\<noteq>a \<longrightarrow> x\<in>S\<longrightarrow> P (f x)"
+    using impP by (metis assms(1) bij_pointE imageI)
+  then show "eventually P (filtermap f (at a within S))" 
+    unfolding eventually_filtermap eventually_at_topological 
+    apply (intro exI[of _ T2])
+    using \<open>open T2\<close> \<open>a \<in> T2\<close> by auto
+qed
+  
 lemma filterlim_at_left_to_right:
   "filterlim f F (at_left a) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
   for a :: real
@@ -2015,6 +2048,32 @@
     by eventually_elim simp
 qed
 
+lemma filterlim_tendsto_add_at_top_iff:
+  assumes f: "(f \<longlongrightarrow> c) F"
+  shows "(LIM x F. (f x + g x :: real) :> at_top) \<longleftrightarrow> (LIM x F. g x :> at_top)"
+proof     
+  assume "LIM x F. f x + g x :> at_top" 
+  moreover have "((\<lambda>x. - f x) \<longlongrightarrow> - c) F"
+    by (simp add: f tendsto_minus)
+  ultimately show "filterlim g at_top F" 
+    using filterlim_tendsto_add_at_top  by fastforce
+qed (auto simp: filterlim_tendsto_add_at_top[OF f])    
+
+lemma filterlim_tendsto_add_at_bot_iff:
+  fixes c::real
+  assumes f: "(f \<longlongrightarrow> c) F"
+  shows "(LIM x F. f x + g x :> at_bot) \<longleftrightarrow> (LIM x F. g x :> at_bot)" 
+proof -
+  have "(LIM x F. f x + g x :> at_bot) 
+        \<longleftrightarrow>  (LIM x F. - f x + (- g x)  :> at_top)"
+    by (simp add: filterlim_uminus_at_bot)
+  also have "... = (LIM x F. - g x  :> at_top)"
+    by (metis f filterlim_tendsto_add_at_top_iff tendsto_minus)
+  also have "... = (LIM x F. g x  :> at_bot)"
+    by (simp add: filterlim_uminus_at_bot)
+  finally show ?thesis .
+qed
+
 lemma LIM_at_top_divide:
   fixes f g :: "'a \<Rightarrow> real"
   assumes f: "(f \<longlongrightarrow> a) F" "0 < a"
diff -r 700f9b01c9d9 -r 5540532087fa src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon May 05 12:42:40 2025 +0200
+++ b/src/HOL/Topological_Spaces.thy	Mon May 05 17:04:14 2025 +0100
@@ -2319,6 +2319,26 @@
   "continuous (at x within A) (f :: 'a :: discrete_topology \<Rightarrow> _)"
   by (auto simp: continuous_def at_discrete)
 
+text \<open>Continuity in terms of open preimages.\<close>
+
+lemma continuous_at_open:
+  "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t \<longrightarrow> (\<exists>S. open S \<and> x \<in> S \<and> (\<forall>x' \<in> S. (f x') \<in> t)))"
+  by (metis UNIV_I continuous_within_topological)
+
+lemma continuous_imp_tendsto:
+  assumes "continuous (at x0) f" and "x \<longlonglongrightarrow> x0"
+  shows "(f \<circ> x) \<longlonglongrightarrow> (f x0)"
+proof (rule topological_tendstoI)
+  fix S
+  assume "open S" "f x0 \<in> S"
+  then obtain T where T_def: "open T" "x0 \<in> T" "\<forall>x\<in>T. f x \<in> S"
+     using assms continuous_at_open by metis
+  then have "eventually (\<lambda>n. x n \<in> T) sequentially"
+    using assms T_def by (auto simp: tendsto_def)
+  then show "eventually (\<lambda>n. (f \<circ> x) n \<in> S) sequentially"
+    using T_def by (auto elim!: eventually_mono)
+qed
+
 abbreviation isCont :: "('a::t2_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> bool"
   where "isCont f a \<equiv> continuous (at a) f"