author paulson Tue, 15 Feb 2022 13:00:05 +0000 changeset 75078 ec86cb2418e1 parent 75076 3bcbc4d12916 child 75079 8a48a9be91ce
an assortment of new or stronger lemmas
 src/HOL/Analysis/Cartesian_Euclidean_Space.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Continuum_Not_Denumerable.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Derivative.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Lebesgue_Measure.thy file | annotate | diff | comparison | revisions src/HOL/Groups_Big.thy file | annotate | diff | comparison | revisions src/HOL/Library/FuncSet.thy file | annotate | diff | comparison | revisions
```--- 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"```
```--- 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"```
```--- 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"```
```--- 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))"```
```--- 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))"```
```--- 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)
```