--- 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"
--- 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>
--- 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)
--- 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"
--- 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"