--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy Fri Jul 07 10:39:28 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy Fri Jul 07 14:05:05 2023 +0100
@@ -144,24 +144,6 @@
by (auto simp: openin_mtopology)
qed
-(*
-lemma metric_injective_image:
- "\<And>f m s.
- f ` s \<subseteq> M \<and>
- (\<forall>x y. x \<in> s \<and> y \<in> s \<and> f x = f y \<Longrightarrow> x = y)
- \<Longrightarrow> (mspace(metric(s,\<lambda>(x,y). d (f x) (f y))) = s) \<and>
- (d(metric(s,\<lambda>(x,y). d (f x) (f y))) =
- \<lambda>(x,y). d (f x) (f y))"
-oops
- REWRITE_TAC[\<subseteq>; FORALL_IN_IMAGE; INJECTIVE_ON_ALT] THEN
- REPEAT GEN_TAC THEN STRIP_TAC THEN
- REWRITE_TAC[mspace; d; GSYM PAIR_EQ] THEN
- REWRITE_TAC[GSYM(CONJUNCT2 metric_tybij); is_metric_space] THEN
- REWRITE_TAC[GSYM mspace; GSYM d] THEN
- ASM_SIMP_TAC[MDIST_POS_LE; MDIST_TRIANGLE; MDIST_0] THEN
- ASM_MESON_TAC[MDIST_SYM]);;
-*)
-
lemma mtopology_base:
"mtopology = topology(arbitrary union_of (\<lambda>U. \<exists>x \<in> M. \<exists>r>0. U = mball x r))"
proof -
@@ -266,8 +248,6 @@
by (metis centre_in_mball_iff gt0 openin_mball topspace_mtopology x y)
qed
-
-
subsection\<open>Bounded sets\<close>
definition mbounded where "mbounded S \<longleftrightarrow> (\<exists>x B. S \<subseteq> mcball x B)"
@@ -656,6 +636,33 @@
lemma (in Metric_space) metrizable_space_mtopology: "metrizable_space mtopology"
using local.Metric_space_axioms metrizable_space_def by blast
+lemma (in Metric_space) first_countable_mtopology: "first_countable mtopology"
+proof (clarsimp simp add: first_countable_def)
+ fix x
+ assume "x \<in> M"
+ define \<B> where "\<B> \<equiv> mball x ` {r \<in> \<rat>. 0 < r}"
+ show "\<exists>\<B>. countable \<B> \<and> (\<forall>V\<in>\<B>. openin mtopology V) \<and> (\<forall>U. openin mtopology U \<and> x \<in> U \<longrightarrow> (\<exists>V\<in>\<B>. x \<in> V \<and> V \<subseteq> U))"
+ proof (intro exI conjI ballI)
+ show "countable \<B>"
+ by (simp add: \<B>_def countable_rat)
+ show "\<forall>U. openin mtopology U \<and> x \<in> U \<longrightarrow> (\<exists>V\<in>\<B>. x \<in> V \<and> V \<subseteq> U)"
+ proof clarify
+ fix U
+ assume "openin mtopology U" and "x \<in> U"
+ then obtain r where "r>0" and r: "mball x r \<subseteq> U"
+ by (meson openin_mtopology)
+ then obtain q where "q \<in> Rats" "0 < q" "q < r"
+ using Rats_dense_in_real by blast
+ then show "\<exists>V\<in>\<B>. x \<in> V \<and> V \<subseteq> U"
+ unfolding \<B>_def using \<open>x \<in> M\<close> r by fastforce
+ qed
+ qed (auto simp: \<B>_def)
+qed
+
+lemma metrizable_imp_first_countable:
+ "metrizable_space X \<Longrightarrow> first_countable X"
+ by (force simp add: metrizable_space_def Metric_space.first_countable_mtopology)
+
lemma openin_mtopology_eq_open [simp]: "openin Met_TC.mtopology = open"
by (simp add: Met_TC.mtopology_def)
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Fri Jul 07 10:39:28 2023 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Fri Jul 07 14:05:05 2023 +0100
@@ -8,10 +8,6 @@
imports Equivalence_Lebesgue_Henstock_Integration Improper_Integral Continuous_Extension
begin
-(*Borrowed from Ergodic_Theory/SG_Library_Complement*)
-abbreviation sym_diff :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "sym_diff A B \<equiv> ((A - B) \<union> (B-A))"
-
subsection\<open>Austin's Lemma\<close>
lemma Austin_Lemma:
--- a/src/HOL/Fun.thy Fri Jul 07 10:39:28 2023 +0200
+++ b/src/HOL/Fun.thy Fri Jul 07 14:05:05 2023 +0100
@@ -218,6 +218,10 @@
lemma inj_onI [intro?]: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x = f y \<Longrightarrow> x = y) \<Longrightarrow> inj_on f A"
by (simp add: inj_on_def)
+text \<open>For those frequent proofs by contradiction\<close>
+lemma inj_onCI: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x = f y \<Longrightarrow> x \<noteq> y \<Longrightarrow> False) \<Longrightarrow> inj_on f A"
+ by (force simp: inj_on_def)
+
lemma inj_on_inverseI: "(\<And>x. x \<in> A \<Longrightarrow> g (f x) = x) \<Longrightarrow> inj_on f A"
by (auto dest: arg_cong [of concl: g] simp add: inj_on_def)
--- a/src/HOL/Set.thy Fri Jul 07 10:39:28 2023 +0200
+++ b/src/HOL/Set.thy Fri Jul 07 14:05:05 2023 +0100
@@ -719,6 +719,9 @@
lemma Compl_eq_Diff_UNIV: "- A = (UNIV - A)"
by blast
+abbreviation sym_diff :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+ "sym_diff A B \<equiv> ((A - B) \<union> (B-A))"
+
subsubsection \<open>Augmenting a set -- \<^const>\<open>insert\<close>\<close>