--- a/src/HOL/Analysis/Complex_Transcendental.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Jan 31 14:05:16 2023 +0000
@@ -2193,6 +2193,12 @@
by (auto simp: Re_exp Im_exp)
qed
+lemma Arg_1 [simp]: "Arg 1 = 0"
+ by (rule Arg_unique[of 1]) auto
+
+lemma Arg_numeral [simp]: "Arg (numeral n) = 0"
+ by (rule Arg_unique[of "numeral n"]) auto
+
lemma Arg_times_of_real [simp]:
assumes "0 < r" shows "Arg (of_real r * z) = Arg z"
using Arg_def Ln_times_of_real assms by auto
@@ -2207,6 +2213,10 @@
using Im_Ln_le_pi Im_Ln_pos_le
by (simp add: Arg_def)
+text \<open>converse fails because the argument can equal $\pi$.\<close>
+lemma Arg_uminus: "Arg z < 0 \<Longrightarrow> Arg (-z) > 0"
+ by (smt (verit) Arg_bounded Arg_minus Complex.Arg_def)
+
lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> Re z < 0 \<and> Im z = 0"
by (auto simp: Arg_def Im_Ln_eq_pi)
@@ -2261,7 +2271,13 @@
by (metis Arg_cnj_eq_inverse Arg_inverse Reals_0 complex_cnj_zero)
lemma Arg_exp: "-pi < Im z \<Longrightarrow> Im z \<le> pi \<Longrightarrow> Arg(exp z) = Im z"
- by (rule Arg_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)
+ by (simp add: Arg_eq_Im_Ln)
+
+lemma Arg_cis: "x \<in> {-pi<..pi} \<Longrightarrow> Arg (cis x) = x"
+ unfolding cis_conv_exp by (subst Arg_exp) auto
+
+lemma Arg_rcis: "x \<in> {-pi<..pi} \<Longrightarrow> r > 0 \<Longrightarrow> Arg (rcis r x) = x"
+ unfolding rcis_def by (subst Arg_times_of_real) (auto simp: Arg_cis)
lemma Ln_Arg: "z\<noteq>0 \<Longrightarrow> Ln(z) = ln(norm z) + \<i> * Arg(z)"
by (metis Arg_def Re_Ln complex_eq)
@@ -3093,6 +3109,33 @@
by simp
qed
+lemma csqrt_mult:
+ assumes "Arg z + Arg w \<in> {-pi<..pi}"
+ shows "csqrt (z * w) = csqrt z * csqrt w"
+proof (cases "z = 0 \<or> w = 0")
+ case False
+ have "csqrt (z * w) = exp ((ln (z * w)) / 2)"
+ using False by (intro csqrt_exp_Ln) auto
+ also have "\<dots> = exp ((Ln z + Ln w) / 2)"
+ using False assms by (subst Ln_times_simple) (auto simp: Arg_eq_Im_Ln)
+ also have "(Ln z + Ln w) / 2 = Ln z / 2 + Ln w / 2"
+ by (simp add: add_divide_distrib)
+ also have "exp \<dots> = csqrt z * csqrt w"
+ using False by (simp add: exp_add csqrt_exp_Ln)
+ finally show ?thesis .
+qed auto
+
+lemma Arg_csqrt [simp]: "Arg (csqrt z) = Arg z / 2"
+proof (cases "z = 0")
+ case False
+ have "Im (Ln z) \<in> {-pi<..pi}"
+ by (simp add: False Im_Ln_le_pi mpi_less_Im_Ln)
+ also have "\<dots> \<subseteq> {-2*pi<..2*pi}"
+ by auto
+ finally show ?thesis
+ using False by (auto simp: csqrt_exp_Ln Arg_exp Arg_eq_Im_Ln)
+qed (auto simp: Arg_zero)
+
lemma csqrt_inverse:
"z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt (inverse z) = inverse (csqrt z)"
by (metis Ln_inverse csqrt_eq_0 csqrt_exp_Ln divide_minus_left exp_minus
--- a/src/HOL/Analysis/Derivative.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Analysis/Derivative.thy Tue Jan 31 14:05:16 2023 +0000
@@ -313,9 +313,13 @@
lemma diff_chain_at[derivative_intros]:
"(f has_derivative f') (at x) \<Longrightarrow>
(g has_derivative g') (at (f x)) \<Longrightarrow> ((g \<circ> f) has_derivative (g' \<circ> f')) (at x)"
- using has_derivative_compose[of f f' x UNIV g g']
- by (simp add: comp_def)
-
+ by (meson diff_chain_within has_derivative_at_withinI)
+
+lemma has_vector_derivative_shift: "(f has_vector_derivative D x) (at x)
+ \<Longrightarrow> ((+) d \<circ> f has_vector_derivative D x) (at x)"
+ using diff_chain_at [OF _ shift_has_derivative_id]
+ by (simp add: has_derivative_iff_Ex has_vector_derivative_def)
+
lemma has_vector_derivative_within_open:
"a \<in> S \<Longrightarrow> open S \<Longrightarrow>
(f has_vector_derivative f') (at a within S) \<longleftrightarrow> (f has_vector_derivative f') (at a)"
@@ -3311,7 +3315,16 @@
lemma C1_differentiable_on_of_real [derivative_intros]: "of_real C1_differentiable_on S"
unfolding C1_differentiable_on_def
- by (smt (verit, del_insts) DERIV_ident UNIV_I continuous_on_const has_vector_derivative_of_real has_vector_derivative_transform)
+ using vector_derivative_works by fastforce
+
+lemma C1_differentiable_on_translation:
+ "f C1_differentiable_on U - S \<Longrightarrow> (+) d \<circ> f C1_differentiable_on U - S"
+ by (metis C1_differentiable_on_def has_vector_derivative_shift)
+
+lemma C1_differentiable_on_translation_eq:
+ fixes d :: "'a::real_normed_vector"
+ shows "(+) d \<circ> f C1_differentiable_on i - S \<longleftrightarrow> f C1_differentiable_on i - S"
+ by (force simp: o_def intro: C1_differentiable_on_translation dest: C1_differentiable_on_translation [of concl: "-d"])
definition\<^marker>\<open>tag important\<close> piecewise_C1_differentiable_on
@@ -3330,6 +3343,11 @@
C1_differentiable_on_def differentiable_def has_vector_derivative_def
intro: has_derivative_at_withinI)
+lemma piecewise_C1_differentiable_on_translation_eq:
+ "((+) d \<circ> f piecewise_C1_differentiable_on i) \<longleftrightarrow> (f piecewise_C1_differentiable_on i)"
+ unfolding piecewise_C1_differentiable_on_def continuous_on_translation_eq
+ by (metis C1_differentiable_on_translation_eq)
+
lemma piecewise_C1_differentiable_compose [derivative_intros]:
assumes fg: "f piecewise_C1_differentiable_on S" "g piecewise_C1_differentiable_on (f ` S)" and fin: "\<And>x. finite (S \<inter> f-`{x})"
shows "(g \<circ> f) piecewise_C1_differentiable_on S"
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Jan 31 14:05:16 2023 +0000
@@ -370,6 +370,20 @@
by (metis islimpt_approachable closed_limpt [where 'a='a])
qed
+lemma discrete_imp_not_islimpt:
+ assumes e: "0 < e"
+ and d: "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> dist y x < e \<Longrightarrow> y = x"
+ shows "\<not> x islimpt S"
+proof
+ assume "x islimpt S"
+ hence "x islimpt S - {x}"
+ by (meson islimpt_punctured)
+ moreover from assms have "closed (S - {x})"
+ by (intro discrete_imp_closed) auto
+ ultimately show False
+ unfolding closed_limpt by blast
+qed
+
subsection \<open>Interior\<close>
--- a/src/HOL/Analysis/Elementary_Topology.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Analysis/Elementary_Topology.thy Tue Jan 31 14:05:16 2023 +0000
@@ -13,7 +13,6 @@
Product_Vector
begin
-
section \<open>Elementary Topology\<close>
@@ -845,6 +844,22 @@
apply (auto simp: open_Int)
done
+lemma open_imp_islimpt:
+ fixes x::"'a:: perfect_space"
+ assumes "open S" "x\<in>S"
+ shows "x islimpt S"
+ using assms interior_eq interior_limit_point by auto
+
+lemma islimpt_Int_eventually:
+ assumes "x islimpt A" "eventually (\<lambda>y. y \<in> B) (at x)"
+ shows "x islimpt A \<inter> B"
+ using assms unfolding islimpt_def eventually_at_filter eventually_nhds
+ by (metis Int_iff UNIV_I open_Int)
+
+lemma islimpt_conv_frequently_at:
+ "x islimpt A \<longleftrightarrow> frequently (\<lambda>y. y \<in> A) (at x)"
+ unfolding islimpt_def eventually_at_filter frequently_def eventually_nhds by blast
+
lemma interior_closed_Un_empty_interior:
assumes cS: "closed S"
and iT: "interior T = {}"
@@ -2435,6 +2450,16 @@
lemma homeomorphism_sym: "homeomorphism S t f g = homeomorphism t S g f"
by (force simp: homeomorphism_def)
+lemma continuous_on_translation_eq:
+ fixes g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_vector"
+ shows "continuous_on A ((+) a \<circ> g) = continuous_on A g"
+proof -
+ have g: "g = (\<lambda>x. -a + x) \<circ> ((\<lambda>x. a + x) \<circ> g)"
+ by (rule ext) simp
+ show ?thesis
+ by (metis (no_types, opaque_lifting) g continuous_on_compose homeomorphism_def homeomorphism_translation)
+qed
+
definition\<^marker>\<open>tag important\<close> homeomorphic :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
(infixr "homeomorphic" 60)
where "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"
--- a/src/HOL/Analysis/Line_Segment.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Analysis/Line_Segment.thy Tue Jan 31 14:05:16 2023 +0000
@@ -914,15 +914,21 @@
qed
qed
+lemma closed_segment_same_fst:
+ "fst a = fst b \<Longrightarrow> closed_segment a b = {fst a} \<times> closed_segment (snd a) (snd b)"
+ by (auto simp: closed_segment_def scaleR_prod_def)
+
+lemma closed_segment_same_snd:
+ "snd a = snd b \<Longrightarrow> closed_segment a b = closed_segment (fst a) (fst b) \<times> {snd a}"
+ by (auto simp: closed_segment_def scaleR_prod_def)
+
lemma subset_oc_segment:
fixes a :: "'a::euclidean_space"
shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
-apply (simp add: subset_open_segment [symmetric])
-apply (rule iffI)
- apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
-apply (meson dual_order.trans segment_open_subset_closed)
-done
+ apply (rule iffI)
+ apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment)
+ by (meson dual_order.trans segment_open_subset_closed subset_open_segment)
lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
--- a/src/HOL/Analysis/Smooth_Paths.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Analysis/Smooth_Paths.thy Tue Jan 31 14:05:16 2023 +0000
@@ -270,6 +270,9 @@
lemma closed_valid_path_image: "valid_path g \<Longrightarrow> closed(path_image g)"
by (metis closed_path_image valid_path_imp_path)
+lemma valid_path_translation_eq: "valid_path ((+)d \<circ> p) \<longleftrightarrow> valid_path p"
+ by (simp add: valid_path_def piecewise_C1_differentiable_on_translation_eq)
+
lemma valid_path_compose:
assumes "valid_path g"
and der: "\<And>x. x \<in> path_image g \<Longrightarrow> f field_differentiable (at x)"
@@ -312,9 +315,8 @@
ultimately have "f \<circ> g C1_differentiable_on {0..1} - S"
using C1_differentiable_on_eq by blast
moreover have "path (f \<circ> g)"
- apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]])
using der
- by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
+ by (simp add: path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]] continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
using \<open>finite S\<close> by auto
qed
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Tue Jan 31 14:05:16 2023 +0000
@@ -411,7 +411,7 @@
card_of_Field_ordIso[of r] ordLeq_ordIso_trans by blast
lemma card_of_Pow: "|A| <o |Pow A|"
- using card_of_ordLess2[of "Pow A" A] Cantors_paradox[of A]
+ using card_of_ordLess2[of "Pow A" A] Cantors_theorem[of A]
Pow_not_empty[of A] by auto
corollary Card_order_Pow:
--- a/src/HOL/Complex.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Complex.thy Tue Jan 31 14:05:16 2023 +0000
@@ -214,8 +214,14 @@
finally show ?thesis .
qed
+lemma surj_Re: "surj Re"
+ by (metis Re_complex_of_real surj_def)
+
+lemma surj_Im: "surj Im"
+ by (metis complex.sel(2) surj_def)
+
lemma complex_Im_fact [simp]: "Im (fact n) = 0"
- by (subst of_nat_fact [symmetric]) (simp only: complex_Im_of_nat)
+ by (metis complex_Im_of_nat of_nat_fact)
lemma Re_prod_Reals: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<real>) \<Longrightarrow> Re (prod f A) = prod (\<lambda>x. Re (f x)) A"
proof (induction A rule: infinite_finite_induct)
@@ -279,6 +285,9 @@
lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
by (metis mult.commute power2_i power_mult)
+lemma i_even_power' [simp]: "even n \<Longrightarrow> \<i> ^ n = (-1) ^ (n div 2)"
+ by (metis dvd_mult_div_cancel power2_i power_mult)
+
lemma Re_i_times [simp]: "Re (\<i> * z) = - Im z"
by simp
@@ -1065,6 +1074,12 @@
using pi_not_less_zero by linarith
qed auto
+lemma cos_Arg: "z \<noteq> 0 \<Longrightarrow> cos (Arg z) = Re z / norm z"
+ by (metis Re_sgn cis.sel(1) cis_Arg)
+
+lemma sin_Arg: "z \<noteq> 0 \<Longrightarrow> sin (Arg z) = Im z / norm z"
+ by (metis Im_sgn cis.sel(2) cis_Arg)
+
subsection \<open>Complex n-th roots\<close>
lemma bij_betw_roots_unity:
--- a/src/HOL/Filter.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Filter.thy Tue Jan 31 14:05:16 2023 +0000
@@ -65,6 +65,9 @@
lemma eventuallyI: "(\<And>x. P x) \<Longrightarrow> eventually P F"
by (auto intro: always_eventually)
+lemma filter_eqI: "(\<And>P. eventually P F \<longleftrightarrow> eventually P G) \<Longrightarrow> F = G"
+ by (auto simp: filter_eq_iff)
+
lemma eventually_mono:
"\<lbrakk>eventually P F; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> eventually Q F"
unfolding eventually_def
@@ -105,6 +108,11 @@
shows "eventually (\<lambda>i. R i) F"
using assms by (auto elim!: eventually_rev_mp)
+lemma eventually_cong:
+ assumes "eventually P F" and "\<And>x. P x \<Longrightarrow> Q x \<longleftrightarrow> R x"
+ shows "eventually Q F \<longleftrightarrow> eventually R F"
+ using assms eventually_elim2 by blast
+
lemma eventually_ball_finite_distrib:
"finite A \<Longrightarrow> (eventually (\<lambda>x. \<forall>y\<in>A. P x y) net) \<longleftrightarrow> (\<forall>y\<in>A. eventually (\<lambda>x. P x y) net)"
by (induction A rule: finite_induct) (auto simp: eventually_conj_iff)
@@ -209,6 +217,12 @@
"(\<exists>\<^sub>Fx in F. P x \<longrightarrow> Q x) \<longleftrightarrow> (eventually P F \<longrightarrow> frequently Q F)"
unfolding imp_conv_disj frequently_disj_iff not_eventually[symmetric] ..
+lemma frequently_eventually_conj:
+ assumes "\<exists>\<^sub>Fx in F. P x"
+ assumes "\<forall>\<^sub>Fx in F. Q x"
+ shows "\<exists>\<^sub>Fx in F. Q x \<and> P x"
+ using assms eventually_elim2 by (force simp add: frequently_def)
+
lemma eventually_frequently_const_simps:
"(\<exists>\<^sub>Fx in F. P x \<and> C) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<and> C"
"(\<exists>\<^sub>Fx in F. C \<and> P x) \<longleftrightarrow> C \<and> (\<exists>\<^sub>Fx in F. P x)"
@@ -557,6 +571,13 @@
apply (auto elim!: eventually_rev_mp)
done
+lemma eventually_comp_filtermap:
+ "eventually (P \<circ> f) F \<longleftrightarrow> eventually P (filtermap f F)"
+ unfolding comp_def using eventually_filtermap by auto
+
+lemma filtermap_compose: "filtermap (f \<circ> g) F = filtermap f (filtermap g F)"
+ unfolding filter_eq_iff by (simp add: eventually_filtermap)
+
lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
by (simp add: filter_eq_iff eventually_filtermap)
@@ -585,6 +606,16 @@
lemma filtermap_INF: "filtermap f (\<Sqinter>b\<in>B. F b) \<le> (\<Sqinter>b\<in>B. filtermap f (F b))"
by (rule INF_greatest, rule filtermap_mono, erule INF_lower)
+lemma frequently_cong:
+ assumes ev: "eventually P F" and QR: "\<And>x. P x \<Longrightarrow> Q x \<longleftrightarrow> R x"
+ shows "frequently Q F \<longleftrightarrow> frequently R F"
+ unfolding frequently_def
+ using QR by (auto intro!: eventually_cong [OF ev])
+
+lemma frequently_filtermap:
+ "frequently P (filtermap f F) = frequently (\<lambda>x. P (f x)) F"
+ by (simp add: frequently_def eventually_filtermap)
+
subsubsection \<open>Contravariant map function for filters\<close>
--- a/src/HOL/Library/Equipollence.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Library/Equipollence.thy Tue Jan 31 14:05:16 2023 +0000
@@ -186,7 +186,7 @@
lemma lesspoll_Pow_self: "A \<prec> Pow A"
unfolding lesspoll_def bij_betw_def eqpoll_def
- by (meson lepoll_Pow_self Cantors_paradox)
+ by (meson lepoll_Pow_self Cantors_theorem)
lemma finite_lesspoll_infinite:
assumes "infinite A" "finite B" shows "B \<prec> A"
--- a/src/HOL/Power.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Power.thy Tue Jan 31 14:05:16 2023 +0000
@@ -89,6 +89,9 @@
lemma power4_eq_xxxx: "x^4 = x * x * x * x"
by (simp add: mult.assoc power_numeral_even)
+lemma power_numeral_reduce: "x ^ numeral n = x * x ^ pred_numeral n"
+ by (simp add: numeral_eq_Suc)
+
lemma funpow_times_power: "(times x ^^ f x) = times (x ^ f x)"
proof (induct "f x" arbitrary: f)
case 0
--- a/src/HOL/Set.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Set.thy Tue Jan 31 14:05:16 2023 +0000
@@ -952,7 +952,7 @@
lemma image_add_0 [simp]: "(+) (0::'a::comm_monoid_add) ` S = S"
by auto
-theorem Cantors_paradox: "\<nexists>f. f ` A = Pow A"
+theorem Cantors_theorem: "\<nexists>f. f ` A = Pow A"
proof
assume "\<exists>f. f ` A = Pow A"
then obtain f where f: "f ` A = Pow A" ..
@@ -1363,7 +1363,7 @@
lemma Diff_Int2: "A \<inter> C - B \<inter> C = A \<inter> C - B"
by blast
-lemma subset_UnE:
+lemma subset_UnE:
assumes "C \<subseteq> A \<union> B"
obtains A' B' where "A' \<subseteq> A" "B' \<subseteq> B" "C = A' \<union> B'"
proof
--- a/src/HOL/Topological_Spaces.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Topological_Spaces.thy Tue Jan 31 14:05:16 2023 +0000
@@ -720,6 +720,24 @@
using linordered_field_no_lb[rule_format, of x]
by (auto simp: eventually_at_left)
+lemma filtermap_nhds_eq_imp_filtermap_at_eq:
+ assumes "filtermap f (nhds z) = nhds (f z)"
+ assumes "eventually (\<lambda>x. f x = f z \<longrightarrow> x = z) (at z)"
+ shows "filtermap f (at z) = at (f z)"
+proof (rule filter_eqI)
+ fix P :: "'a \<Rightarrow> bool"
+ have "eventually P (filtermap f (at z)) \<longleftrightarrow> (\<forall>\<^sub>F x in nhds z. x \<noteq> z \<longrightarrow> P (f x))"
+ by (simp add: eventually_filtermap eventually_at_filter)
+ also have "\<dots> \<longleftrightarrow> (\<forall>\<^sub>F x in nhds z. f x \<noteq> f z \<longrightarrow> P (f x))"
+ by (rule eventually_cong [OF assms(2)[unfolded eventually_at_filter]]) auto
+ also have "\<dots> \<longleftrightarrow> (\<forall>\<^sub>F x in filtermap f (nhds z). x \<noteq> f z \<longrightarrow> P x)"
+ by (simp add: eventually_filtermap)
+ also have "filtermap f (nhds z) = nhds (f z)"
+ by (rule assms)
+ also have "(\<forall>\<^sub>F x in nhds (f z). x \<noteq> f z \<longrightarrow> P x) \<longleftrightarrow> (\<forall>\<^sub>F x in at (f z). P x)"
+ by (simp add: eventually_at_filter)
+ finally show "eventually P (filtermap f (at z)) = eventually P (at (f z))" .
+qed
subsubsection \<open>Tendsto\<close>
@@ -1803,6 +1821,29 @@
by (metis (no_types) f filterlim_compose filterlim_filtermap g tendsto_at_iff_tendsto_nhds tendsto_compose_filtermap)
qed
+lemma tendsto_nhds_iff: "(f \<longlongrightarrow> (c :: 'a :: t1_space)) (nhds x) \<longleftrightarrow> f \<midarrow>x\<rightarrow> c \<and> f x = c"
+proof safe
+ assume lim: "(f \<longlongrightarrow> c) (nhds x)"
+ show "f x = c"
+ proof (rule ccontr)
+ assume "f x \<noteq> c"
+ hence "c \<noteq> f x"
+ by auto
+ then obtain A where A: "open A" "c \<in> A" "f x \<notin> A"
+ by (subst (asm) separation_t1) auto
+ with lim obtain B where "open B" "x \<in> B" "\<And>x. x \<in> B \<Longrightarrow> f x \<in> A"
+ unfolding tendsto_def eventually_nhds by metis
+ with \<open>f x \<notin> A\<close> show False
+ by blast
+ qed
+ show "(f \<longlongrightarrow> c) (at x)"
+ using lim by (rule filterlim_mono) (auto simp: at_within_def)
+next
+ assume "f \<midarrow>x\<rightarrow> f x" "c = f x"
+ thus "(f \<longlongrightarrow> f x) (nhds x)"
+ unfolding tendsto_def eventually_at_filter by (fast elim: eventually_mono)
+qed
+
subsubsection \<open>Relation of \<open>LIM\<close> and \<open>LIMSEQ\<close>\<close>
@@ -2289,20 +2330,35 @@
"isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
using continuous_at_imp_continuous_at_within continuous_within_compose2 by blast
-lemma filtermap_nhds_open_map:
+lemma filtermap_nhds_open_map':
assumes cont: "isCont f a"
- and open_map: "\<And>S. open S \<Longrightarrow> open (f`S)"
+ and "open A" "a \<in> A"
+ and open_map: "\<And>S. open S \<Longrightarrow> S \<subseteq> A \<Longrightarrow> open (f ` S)"
shows "filtermap f (nhds a) = nhds (f a)"
unfolding filter_eq_iff
proof safe
fix P
assume "eventually P (filtermap f (nhds a))"
- then obtain S where "open S" "a \<in> S" "\<forall>x\<in>S. P (f x)"
+ then obtain S where S: "open S" "a \<in> S" "\<forall>x\<in>S. P (f x)"
by (auto simp: eventually_filtermap eventually_nhds)
- then show "eventually P (nhds (f a))"
- unfolding eventually_nhds by (intro exI[of _ "f`S"]) (auto intro!: open_map)
+ show "eventually P (nhds (f a))"
+ unfolding eventually_nhds
+ proof (rule exI [of _ "f ` (A \<inter> S)"], safe)
+ show "open (f ` (A \<inter> S))"
+ using S by (intro open_Int assms) auto
+ show "f a \<in> f ` (A \<inter> S)"
+ using assms S by auto
+ show "P (f x)" if "x \<in> A" "x \<in> S" for x
+ using S that by auto
+ qed
qed (metis filterlim_iff tendsto_at_iff_tendsto_nhds isCont_def eventually_filtermap cont)
+lemma filtermap_nhds_open_map:
+ assumes cont: "isCont f a"
+ and open_map: "\<And>S. open S \<Longrightarrow> open (f`S)"
+ shows "filtermap f (nhds a) = nhds (f a)"
+ using cont filtermap_nhds_open_map' open_map by blast
+
lemma continuous_at_split:
"continuous (at x) f \<longleftrightarrow> continuous (at_left x) f \<and> continuous (at_right x) f"
for x :: "'a::linorder_topology"
--- a/src/HOL/Transcendental.thy Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Transcendental.thy Tue Jan 31 14:05:16 2023 +0000
@@ -1531,6 +1531,28 @@
qed
qed simp
+lemma exp_power_int:
+ fixes x :: "'a::{real_normed_field,banach}"
+ shows "exp x powi n = exp (of_int n * x)"
+proof (cases "n \<ge> 0")
+ case True
+ have "exp x powi n = exp x ^ nat n"
+ using True by (simp add: power_int_def)
+ thus ?thesis
+ using True by (subst (asm) exp_of_nat_mult [symmetric]) auto
+next
+ case False
+ have "exp x powi n = inverse (exp x ^ nat (-n))"
+ using False by (simp add: power_int_def field_simps)
+ also have "exp x ^ nat (-n) = exp (of_nat (nat (-n)) * x)"
+ using False by (subst exp_of_nat_mult) auto
+ also have "inverse \<dots> = exp (-(of_nat (nat (-n)) * x))"
+ by (subst exp_minus) (auto simp: field_simps)
+ also have "-(of_nat (nat (-n)) * x) = of_int n * x"
+ using False by simp
+ finally show ?thesis .
+qed
+
subsubsection \<open>Properties of the Exponential Function on Reals\<close>
@@ -2493,6 +2515,9 @@
lemma powr_realpow: "0 < x \<Longrightarrow> x powr (real n) = x^n"
by (induction n) (simp_all add: ac_simps powr_add)
+lemma powr_realpow': "(z :: real) \<ge> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> z powr of_nat n = z ^ n"
+ by (cases "z = 0") (auto simp: powr_realpow)
+
lemma powr_real_of_int':
assumes "x \<ge> 0" "x \<noteq> 0 \<or> n > 0"
shows "x powr real_of_int n = power_int x n"