--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Tue Feb 15 16:16:53 2022 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Tue Feb 15 16:42:15 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 Tue Feb 15 16:16:53 2022 +0100
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy Tue Feb 15 16:42:15 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 Tue Feb 15 16:16:53 2022 +0100
+++ b/src/HOL/Analysis/Derivative.thy Tue Feb 15 16:42:15 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 Tue Feb 15 16:16:53 2022 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Tue Feb 15 16:42:15 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 Tue Feb 15 16:16:53 2022 +0100
+++ b/src/HOL/Groups_Big.thy Tue Feb 15 16:42:15 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 Tue Feb 15 16:16:53 2022 +0100
+++ b/src/HOL/Library/FuncSet.thy Tue Feb 15 16:42:15 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)