# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1745412158 -7200
# Node ID 32a6228f543d89b45c5e4d15def8f76abfe1c03f
# Parent  5160b68e78a959613eaccab7f933772593a29a64
a few small lemmas for HOL and HOL-Analysis

diff -r 5160b68e78a9 -r 32a6228f543d src/HOL/Analysis/Infinite_Sum.thy
--- a/src/HOL/Analysis/Infinite_Sum.thy	Wed Apr 23 01:38:06 2025 +0200
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Wed Apr 23 14:42:38 2025 +0200
@@ -2845,6 +2845,31 @@
   using has_sum_reindex_bij_witness[of S i j T h g, OF assms]
   by (simp add: summable_on_def)
 
+lemma infsum_reindex_bij_witness:
+  assumes "\<And>a. a \<in> S \<Longrightarrow> i (j a) = a"
+  assumes "\<And>a. a \<in> S \<Longrightarrow> j a \<in> T"
+  assumes "\<And>b. b \<in> T \<Longrightarrow> j (i b) = b"
+  assumes "\<And>b. b \<in> T \<Longrightarrow> i b \<in> S"
+  assumes "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
+  shows   "infsum g S = infsum h T"
+proof (cases "g summable_on S")
+  case True
+  then obtain s where s: "(g has_sum s) S"
+    by (auto simp: summable_on_def)
+  also have "?this \<longleftrightarrow> (h has_sum s) T"
+    by (rule has_sum_reindex_bij_witness[of _ i j]) (use assms in auto)
+  finally have s': "(h has_sum s) T" .
+  show ?thesis
+    using infsumI[OF s] infsumI[OF s'] by simp
+next
+  case False
+  note \<open>\<not>g summable_on S\<close>
+  also have "g summable_on S \<longleftrightarrow> h summable_on T"
+    by (rule summable_on_reindex_bij_witness[of _ i j]) (use assms in auto)
+  finally show ?thesis
+    using False by (simp add: infsum_not_exists)
+qed
+
 lemma has_sum_homomorphism:
   assumes "(f has_sum S) A" "h 0 = 0" "\<And>a b. h (a + b) = h a + h b" "continuous_on UNIV h"
   shows   "((\<lambda>x. h (f x)) has_sum (h S)) A"
diff -r 5160b68e78a9 -r 32a6228f543d src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Wed Apr 23 01:38:06 2025 +0200
+++ b/src/HOL/Archimedean_Field.thy	Wed Apr 23 14:42:38 2025 +0200
@@ -705,6 +705,9 @@
 lemma frac_eq: "frac x = x \<longleftrightarrow> 0 \<le> x \<and> x < 1"
   by (simp add: frac_unique_iff)
 
+lemma frac_eq_id [simp]: "x \<in> {0..<1} \<Longrightarrow> frac x = x"
+  by (simp add: frac_eq)
+
 lemma frac_neg: "frac (- x) = (if x \<in> \<int> then 0 else 1 - frac x)"
   for x :: "'a::floor_ceiling"
   apply (auto simp add: frac_unique_iff)
diff -r 5160b68e78a9 -r 32a6228f543d src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Apr 23 01:38:06 2025 +0200
+++ b/src/HOL/Product_Type.thy	Wed Apr 23 14:42:38 2025 +0200
@@ -1316,6 +1316,11 @@
     by auto
 qed
 
+lemma bij_betw_map_prod:
+  assumes "bij_betw f A C" "bij_betw g B D"
+  shows   "bij_betw (map_prod f g) (A \<times> B) (C \<times> D)"
+  using assms unfolding bij_betw_def inj_on_def by auto
+
 
 subsection \<open>Simproc for rewriting a set comprehension into a pointfree expression\<close>