# HG changeset patch
# User wenzelm
# Date 1688827695 -7200
# Node ID 45a9f5066e07bc5b93cb24109bbdcdf955585b04
# Parent  45381e6bd3adffeca8095125d0d2d048212d7c62# Parent  4be047eaee2ba8aa682614d82c0aa8f287eaf020
merged

diff -r 4be047eaee2b -r 45a9f5066e07 src/HOL/Analysis/Abstract_Metric_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Sat Jul 08 16:07:45 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Sat Jul 08 16:48:15 2023 +0200
@@ -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)
 
diff -r 4be047eaee2b -r 45a9f5066e07 src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Sat Jul 08 16:07:45 2023 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Sat Jul 08 16:48:15 2023 +0200
@@ -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:
diff -r 4be047eaee2b -r 45a9f5066e07 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sat Jul 08 16:07:45 2023 +0200
+++ b/src/HOL/Fun.thy	Sat Jul 08 16:48:15 2023 +0200
@@ -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)
 
diff -r 4be047eaee2b -r 45a9f5066e07 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Jul 08 16:07:45 2023 +0200
+++ b/src/HOL/Set.thy	Sat Jul 08 16:48:15 2023 +0200
@@ -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>