--- a/src/HOL/Analysis/Abstract_Topology_2.thy Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy Sat Sep 23 18:45:19 2023 +0100
@@ -16,8 +16,8 @@
text \<open>Combination of Elementary and Abstract Topology\<close>
lemma approachable_lt_le2:
- "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
-by (meson dense less_eq_real_def order_le_less_trans)
+ "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
+ by (meson dense less_eq_real_def order_le_less_trans)
lemma triangle_lemma:
fixes x y z :: real
@@ -113,7 +113,7 @@
lemma connected_as_closed_union:
assumes "connected C" "C = A \<union> B" "closed A" "closed B" "A \<noteq> {}" "B \<noteq> {}"
shows "A \<inter> B \<noteq> {}"
-by (metis assms closed_Un connected_closed_set)
+ by (metis assms closed_Un connected_closed_set)
lemma closedin_subset_trans:
"closedin (top_of_set U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow>
@@ -126,13 +126,13 @@
by (auto simp: openin_open)
lemma closedin_compact:
- "\<lbrakk>compact S; closedin (top_of_set S) T\<rbrakk> \<Longrightarrow> compact T"
-by (metis closedin_closed compact_Int_closed)
+ "\<lbrakk>compact S; closedin (top_of_set S) T\<rbrakk> \<Longrightarrow> compact T"
+ by (metis closedin_closed compact_Int_closed)
lemma closedin_compact_eq:
fixes S :: "'a::t2_space set"
shows "compact S \<Longrightarrow> (closedin (top_of_set S) T \<longleftrightarrow> compact T \<and> T \<subseteq> S)"
-by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
+ by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
subsection \<open>Closure\<close>
@@ -304,6 +304,11 @@
then show ?thesis by auto
qed
+lemma continuous_image_closure_subset:
+ assumes "continuous_on A f" "closure B \<subseteq> A"
+ shows "f ` closure B \<subseteq> closure (f ` B)"
+ using assms by (meson closed_closure closure_subset continuous_on_subset image_closure_subset)
+
subsection\<^marker>\<open>tag unimportant\<close> \<open>A function constant on a set\<close>
definition constant_on (infixl "(constant'_on)" 50)
--- a/src/HOL/Complex.thy Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Complex.thy Sat Sep 23 18:45:19 2023 +0100
@@ -464,6 +464,10 @@
lemmas Re_suminf = bounded_linear.suminf[OF bounded_linear_Re]
lemmas Im_suminf = bounded_linear.suminf[OF bounded_linear_Im]
+lemma continuous_on_Complex [continuous_intros]:
+ "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. Complex (f x) (g x))"
+ unfolding Complex_eq by (intro continuous_intros)
+
lemma tendsto_Complex [tendsto_intros]:
"(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) \<longlongrightarrow> Complex a b) F"
unfolding Complex_eq by (auto intro!: tendsto_intros)
@@ -872,9 +876,6 @@
lemma i_not_in_Reals [simp, intro]: "\<i> \<notin> \<real>"
by (auto simp: complex_is_Real_iff)
-lemma powr_power_complex: "z \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> (z powr u :: complex) ^ n = z powr (of_nat n * u)"
- by (induction n) (auto simp: algebra_simps powr_add)
-
lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re (cis a ^ n)"
by (auto simp add: DeMoivre)
--- a/src/HOL/Int.thy Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Int.thy Sat Sep 23 18:45:19 2023 +0100
@@ -1487,6 +1487,9 @@
using pos_zmult_eq_1_iff_lemma [OF L] L by force
qed auto
+lemma zmult_eq_neg1_iff: "a * b = (-1 :: int) \<longleftrightarrow> a = 1 \<and> b = -1 \<or> a = -1 \<and> b = 1"
+ using zmult_eq_1_iff[of a "-b"] by auto
+
lemma infinite_UNIV_int [simp]: "\<not> finite (UNIV::int set)"
proof
assume "finite (UNIV::int set)"
--- a/src/HOL/Topological_Spaces.thy Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Topological_Spaces.thy Sat Sep 23 18:45:19 2023 +0100
@@ -1076,38 +1076,12 @@
unfolding Lim_def using tendsto_unique [of net f] by auto
lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
- by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
+ by (simp add: tendsto_Lim)
lemma Lim_cong:
- assumes "eventually (\<lambda>x. f x = g x) F" "F = G"
- shows "Lim F f = Lim G g"
-proof (cases "(\<exists>c. (f \<longlongrightarrow> c) F) \<and> F \<noteq> bot")
- case True
- then obtain c where c: "(f \<longlongrightarrow> c) F"
- by blast
- hence "Lim F f = c"
- using True by (intro tendsto_Lim) auto
- moreover have "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) G"
- using assms by (intro filterlim_cong) auto
- with True c assms have "Lim G g = c"
- by (intro tendsto_Lim) auto
- ultimately show ?thesis
- by simp
-next
- case False
- show ?thesis
- proof (cases "F = bot")
- case True
- thus ?thesis using assms
- by (auto simp: Topological_Spaces.Lim_def)
- next
- case False
- have "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) G" for c
- using assms by (intro filterlim_cong) auto
- thus ?thesis
- by (auto simp: Topological_Spaces.Lim_def)
- qed
-qed
+ assumes "\<forall>\<^sub>F x in F. f x = g x" "F = G"
+ shows "Lim F f = Lim F g"
+ unfolding t2_space_class.Lim_def using tendsto_cong assms by fastforce
lemma eventually_Lim_ident_at:
"(\<forall>\<^sub>F y in at x within X. P (Lim (at x within X) (\<lambda>x. x)) y) \<longleftrightarrow>
--- a/src/HOL/Transcendental.thy Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Transcendental.thy Sat Sep 23 18:45:19 2023 +0100
@@ -2480,6 +2480,11 @@
for a b x :: real
by (simp add: powr_def)
+lemma powr_power:
+ fixes z:: "'a::{real_normed_field,ln}"
+ shows "z \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> (z powr u) ^ n = z powr (of_nat n * u)"
+ by (induction n) (auto simp: algebra_simps powr_add)
+
lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
for a b x :: real
by (simp add: powr_powr mult.commute)