# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1644930005 0
# Node ID ec86cb2418e15c815d7aa262d5baf7ecafb26c38
# Parent  3bcbc4d12916b6fba1c6e2698e31bcf2c10000af
an assortment of new or stronger lemmas

diff -r 3bcbc4d12916 -r ec86cb2418e1 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Feb 14 16:41:48 2022 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Tue Feb 15 13:00:05 2022 +0000
@@ -175,12 +175,18 @@
   finally show "norm (A *v x) \<le> CARD('m) * real (CARD('n)) * B * norm x" .
 qed
 
-
 lemma rational_approximation:
   assumes "e > 0"
   obtains r::real where "r \<in> \<rat>" "\<bar>r - x\<bar> < e"
   using Rats_dense_in_real [of "x - e/2" "x + e/2"] assms by auto
 
+lemma Rats_closure_real: "closure \<rat> = (UNIV::real set)"
+proof -
+  have "\<And>x::real. x \<in> closure \<rat>"
+    by (metis closure_approachable dist_real_def rational_approximation)
+  then show ?thesis by auto
+qed
+
 proposition matrix_rational_approximation:
   fixes A :: "real^'n^'m"
   assumes "e > 0"
diff -r 3bcbc4d12916 -r ec86cb2418e1 src/HOL/Analysis/Continuum_Not_Denumerable.thy
--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Mon Feb 14 16:41:48 2022 +0100
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Tue Feb 15 13:00:05 2022 +0000
@@ -97,6 +97,12 @@
 lemma uncountable_UNIV_real: "uncountable (UNIV :: real set)"
   using real_non_denum unfolding uncountable_def by auto
 
+corollary complex_non_denum: "\<nexists>f :: nat \<Rightarrow> complex. surj f"
+  by (metis (full_types) Re_complex_of_real comp_surj real_non_denum surj_def)
+
+lemma uncountable_UNIV_complex: "uncountable (UNIV :: complex set)"
+  using complex_non_denum unfolding uncountable_def by auto
+
 lemma bij_betw_open_intervals:
   fixes a b c d :: real
   assumes "a < b" "c < d"
diff -r 3bcbc4d12916 -r ec86cb2418e1 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Mon Feb 14 16:41:48 2022 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Tue Feb 15 13:00:05 2022 +0000
@@ -2058,8 +2058,11 @@
 
 lemma field_differentiable_minus [derivative_intros]:
   "f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
-  unfolding field_differentiable_def
-  by (metis field_differentiable_minus)
+  unfolding field_differentiable_def by (metis field_differentiable_minus)
+
+lemma field_differentiable_diff_const [simp,derivative_intros]:
+  "(-)c field_differentiable F"
+  unfolding field_differentiable_def by (rule derivative_eq_intros exI | force)+
 
 lemma field_differentiable_add [derivative_intros]:
   assumes "f field_differentiable F" "g field_differentiable F"
diff -r 3bcbc4d12916 -r ec86cb2418e1 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Feb 14 16:41:48 2022 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Tue Feb 15 13:00:05 2022 +0000
@@ -1729,6 +1729,14 @@
 inductive\<^marker>\<open>tag important\<close> gdelta :: "'a::topological_space set \<Rightarrow> bool" where
   "(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (\<Inter>(F ` UNIV))"
 
+lemma fsigma_UNIV [iff]: "fsigma (UNIV :: 'a::real_inner set)"
+proof -
+  have "(UNIV ::'a set) = (\<Union>i. cball 0 (of_nat i))"
+    by (auto simp: real_arch_simple)
+  then show ?thesis
+    by (metis closed_cball fsigma.intros)
+qed
+
 lemma fsigma_Union_compact:
   fixes S :: "'a::{real_normed_vector,heine_borel} set"
   shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = \<Union>(F ` UNIV))"
diff -r 3bcbc4d12916 -r ec86cb2418e1 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Mon Feb 14 16:41:48 2022 +0100
+++ b/src/HOL/Groups_Big.thy	Tue Feb 15 13:00:05 2022 +0000
@@ -1226,7 +1226,7 @@
     using assms card_eq_0_iff finite_UnionD by fastforce
 qed
 
-lemma card_Union_le_sum_card:
+lemma card_Union_le_sum_card_weak:
   fixes U :: "'a set set"
   assumes "\<forall>u \<in> U. finite u"
   shows "card (\<Union>U) \<le> sum card U"
@@ -1249,6 +1249,11 @@
   qed
 qed
 
+lemma card_Union_le_sum_card:
+  fixes U :: "'a set set"
+  shows "card (\<Union>U) \<le> sum card U"
+  by (metis Union_upper card.infinite card_Union_le_sum_card_weak finite_subset zero_le)
+
 lemma card_UN_le:
   assumes "finite I"
   shows "card(\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. card(A i))"
diff -r 3bcbc4d12916 -r ec86cb2418e1 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Mon Feb 14 16:41:48 2022 +0100
+++ b/src/HOL/Library/FuncSet.thy	Tue Feb 15 13:00:05 2022 +0000
@@ -190,9 +190,12 @@
 lemma restrict_UNIV: "restrict f UNIV = f"
   by (simp add: restrict_def)
 
-lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
+lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A \<longleftrightarrow> inj_on f A"
   by (simp add: inj_on_def restrict_def)
 
+lemma inj_on_restrict_iff: "A \<subseteq> B \<Longrightarrow> inj_on (restrict f B) A \<longleftrightarrow> inj_on f A"
+  by (metis inj_on_cong restrict_def subset_iff)
+
 lemma Id_compose: "f \<in> A \<rightarrow> B \<Longrightarrow> f \<in> extensional A \<Longrightarrow> compose A (\<lambda>y\<in>B. y) f = f"
   by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)