# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1683028265 -3600
# Node ID 01c88cf514fcfc704246cb164d27c62a551a5dc1
# Parent  0649ff183dcf338462a1710b05a1b08afa25255f
A few new theorems

diff -r 0649ff183dcf -r 01c88cf514fc src/HOL/Analysis/Abstract_Limits.thy
--- a/src/HOL/Analysis/Abstract_Limits.thy	Tue May 02 11:09:18 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Limits.thy	Tue May 02 12:51:05 2023 +0100
@@ -47,6 +47,9 @@
 definition limitin :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
   "limitin X f l F \<equiv> l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> eventually (\<lambda>x. f x \<in> U) F)"
 
+lemma limitinD: "\<lbrakk>limitin X f l F; openin X U; l \<in> U\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. f x \<in> U) F"
+  by (simp add: limitin_def)
+
 lemma limitin_canonical_iff [simp]: "limitin euclidean f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
   by (auto simp: limitin_def tendsto_def)
 
diff -r 0649ff183dcf -r 01c88cf514fc src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Tue May 02 11:09:18 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Tue May 02 12:51:05 2023 +0100
@@ -174,6 +174,18 @@
   shows "closedin U (S - T)"
   by (metis Int_Diff cT closedin_Int closedin_subset inf.orderE oS openin_closedin_eq)
 
+lemma all_openin: "(\<forall>U. openin X U \<longrightarrow> P U) \<longleftrightarrow> (\<forall>U. closedin X U \<longrightarrow> P (topspace X - U))"
+  by (metis Diff_Diff_Int closedin_def inf.absorb_iff2 openin_closedin_eq)
+
+lemma all_closedin: "(\<forall>U. closedin X U \<longrightarrow> P U) \<longleftrightarrow> (\<forall>U. openin X U \<longrightarrow> P (topspace X - U))"
+  by (metis Diff_Diff_Int closedin_subset inf.absorb_iff2 openin_closedin_eq)
+
+lemma ex_openin: "(\<exists>U. openin X U \<and> P U) \<longleftrightarrow> (\<exists>U. closedin X U \<and> P (topspace X - U))"
+  by (metis Diff_Diff_Int closedin_def inf.absorb_iff2 openin_closedin_eq)
+
+lemma ex_closedin: "(\<exists>U. closedin X U \<and> P U) \<longleftrightarrow> (\<exists>U. openin X U \<and> P (topspace X - U))"
+  by (metis Diff_Diff_Int closedin_subset inf.absorb_iff2 openin_closedin_eq)
+
 
 subsection\<open>The discrete topology\<close>
 
@@ -1371,7 +1383,7 @@
   by (metis (mono_tags) closedin_closure_of closedin_locally_finite_Union imageE locally_finite_in_closure)
 
 lemma closure_of_Union_subset: "\<Union>((\<lambda>S. X closure_of S) ` \<A>) \<subseteq> X closure_of (\<Union>\<A>)"
-  by clarify (meson Union_upper closure_of_mono subsetD)
+  by (simp add: SUP_le_iff Sup_upper closure_of_mono)
 
 lemma closure_of_locally_finite_Union:
   assumes "locally_finite_in X \<A>" 
@@ -2966,7 +2978,7 @@
     by (metis closure_of_eq)
 qed
 
-lemma connectedin_inter_frontier_of:
+lemma connectedin_Int_frontier_of:
   assumes "connectedin X S" "S \<inter> T \<noteq> {}" "S - T \<noteq> {}"
   shows "S \<inter> X frontier_of T \<noteq> {}"
 proof -
@@ -3360,7 +3372,7 @@
 corollary compact_space_imp_nest:
   fixes C :: "nat \<Rightarrow> 'a set"
   assumes "compact_space X" and clo: "\<And>n. closedin X (C n)"
-    and ne: "\<And>n. C n \<noteq> {}" and inc: "\<And>m n. m \<le> n \<Longrightarrow> C n \<subseteq> C m"
+    and ne: "\<And>n. C n \<noteq> {}" and dec: "decseq C"
   shows "(\<Inter>n. C n) \<noteq> {}"
 proof -
   let ?\<U> = "range (\<lambda>n. \<Inter>m \<le> n. C m)"
@@ -3370,8 +3382,8 @@
   proof -
     obtain n where "\<And>k. k \<in> K \<Longrightarrow> k \<le> n"
       using Max.coboundedI \<open>finite K\<close> by blast
-    with inc have "C n \<subseteq> (\<Inter>n\<in>K. \<Inter>m \<le> n. C m)"
-    by blast
+    with dec have "C n \<subseteq> (\<Inter>n\<in>K. \<Inter>m \<le> n. C m)"
+      unfolding decseq_def by blast
   with ne [of n] show ?thesis
     by blast
   qed
diff -r 0649ff183dcf -r 01c88cf514fc src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Tue May 02 11:09:18 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Tue May 02 12:51:05 2023 +0100
@@ -1138,6 +1138,20 @@
     by (force simp: retract_of_space_def)
 qed
 
+lemma retract_of_space_trans:
+  assumes "S retract_of_space X"  "T retract_of_space subtopology X S"
+  shows "T retract_of_space X"
+  using assms
+  apply (simp add: retract_of_space_retraction_maps)
+  by (metis id_comp inf.absorb_iff2 retraction_maps_compose subtopology_subtopology)
+
+lemma retract_of_space_subtopology:
+  assumes "S retract_of_space X"  "S \<subseteq> U"
+  shows "S retract_of_space subtopology X U"
+  using assms
+  apply (clarsimp simp: retract_of_space_def)
+  by (metis continuous_map_from_subtopology inf.absorb2 subtopology_subtopology)
+
 lemma retract_of_space_clopen:
   assumes "openin X S" "closedin X S" "S = {} \<Longrightarrow> topspace X = {}"
   shows "S retract_of_space X"
@@ -1194,6 +1208,13 @@
   using embedding_map_imp_homeomorphic_space homeomorphic_space_sym section_imp_embedding_map
         section_map_def by blast
 
+lemma hereditary_imp_retractive_property:
+  assumes "\<And>X S. P X \<Longrightarrow> P(subtopology X S)" 
+          "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> Q X')"
+  assumes "retraction_map X X' r" "P X"
+  shows "Q X'"
+  by (meson assms retraction_map_def retraction_maps_section_image2)
+
 subsection\<open>Paths and path-connectedness\<close>
 
 definition pathin :: "'a topology \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool" where
diff -r 0649ff183dcf -r 01c88cf514fc src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Tue May 02 11:09:18 2023 +0100
+++ b/src/HOL/Archimedean_Field.thy	Tue May 02 12:51:05 2023 +0100
@@ -16,15 +16,10 @@
 proof -
   have "Sup (uminus ` S) = - (Inf S)"
   proof (rule antisym)
-    show "- (Inf S) \<le> Sup (uminus ` S)"
-      apply (subst minus_le_iff)
-      apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
-      apply (subst minus_le_iff)
-      apply (rule cSup_upper)
-       apply force
-      using bdd
-      apply (force simp: abs_le_iff bdd_above_def)
-      done
+    have "\<And>x. x \<in> S \<Longrightarrow> bdd_above (uminus ` S)"
+      using bdd by (force simp: abs_le_iff bdd_above_def)
+  then show "- (Inf S) \<le> Sup (uminus ` S)"
+    by (meson cInf_greatest [OF \<open>S \<noteq> {}\<close>] cSUP_upper minus_le_iff)
   next
     have *: "\<And>x. x \<in> S \<Longrightarrow> Inf S \<le> x"
       by (meson abs_le_iff bdd bdd_below_def cInf_lower minus_le_iff)
diff -r 0649ff183dcf -r 01c88cf514fc src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue May 02 11:09:18 2023 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue May 02 12:51:05 2023 +0100
@@ -481,6 +481,12 @@
   assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
 qed (intro cSup_eq_non_empty assms)
 
+lemma cSup_unique:
+  fixes b :: "'a :: {conditionally_complete_lattice, no_bot}"
+  assumes "\<And>c. (\<forall>x \<in> s. x \<le> c) \<longleftrightarrow> b \<le> c"
+  shows "Sup s = b"
+  by (metis assms cSup_eq order.refl)
+
 lemma cInf_eq:
   fixes a :: "'a :: {conditionally_complete_lattice, no_top}"
   assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
@@ -490,6 +496,12 @@
   assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
 qed (intro cInf_eq_non_empty assms)
 
+lemma cInf_unique:
+  fixes b :: "'a :: {conditionally_complete_lattice, no_top}"
+  assumes "\<And>c. (\<forall>x \<in> s. x \<ge> c) \<longleftrightarrow> b \<ge> c"
+  shows "Inf s = b"
+  by (meson assms cInf_eq order.refl)
+
 class conditionally_complete_linorder = conditionally_complete_lattice + linorder
 begin
 
diff -r 0649ff183dcf -r 01c88cf514fc src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue May 02 11:09:18 2023 +0100
+++ b/src/HOL/Fun.thy	Tue May 02 12:51:05 2023 +0100
@@ -1031,6 +1031,12 @@
 abbreviation strict_mono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
   where "strict_mono_on A \<equiv> monotone_on A (<) (<)"
 
+abbreviation antimono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
+  where "antimono_on A \<equiv> monotone_on A (\<le>) (\<ge>)"
+
+abbreviation strict_antimono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
+  where "strict_antimono_on A \<equiv> monotone_on A (<) (>)"
+
 lemma mono_on_def[no_atp]: "mono_on A f \<longleftrightarrow> (\<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s)"
   by (auto simp add: monotone_on_def)
 
@@ -1265,6 +1271,32 @@
   "strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) \<Longrightarrow> mono_on A f"
   by (rule mono_onI, rule strict_mono_on_leD)
 
+lemma mono_imp_strict_mono:
+  fixes f :: "'a::order \<Rightarrow> 'b::order"
+  shows "\<lbrakk>mono_on S f; inj_on f S\<rbrakk> \<Longrightarrow> strict_mono_on S f"
+  by (auto simp add: monotone_on_def order_less_le inj_on_eq_iff)
+
+lemma strict_mono_iff_mono:
+  fixes f :: "'a::linorder \<Rightarrow> 'b::order"
+  shows "strict_mono_on S f \<longleftrightarrow> mono_on S f \<and> inj_on f S"
+proof
+  show "strict_mono_on S f \<Longrightarrow> mono_on S f \<and> inj_on f S"
+    by (simp add: strict_mono_on_imp_inj_on strict_mono_on_imp_mono_on)
+qed (auto intro: mono_imp_strict_mono)
+
+lemma antimono_imp_strict_antimono:
+  fixes f :: "'a::order \<Rightarrow> 'b::order"
+  shows "\<lbrakk>antimono_on S f; inj_on f S\<rbrakk> \<Longrightarrow> strict_antimono_on S f"
+  by (auto simp add: monotone_on_def order_less_le inj_on_eq_iff)
+
+lemma strict_antimono_iff_antimono:
+  fixes f :: "'a::linorder \<Rightarrow> 'b::order"
+  shows "strict_antimono_on S f \<longleftrightarrow> antimono_on S f \<and> inj_on f S"
+proof
+  show "strict_antimono_on S f \<Longrightarrow> antimono_on S f \<and> inj_on f S"
+    by (force simp add: monotone_on_def intro: linorder_inj_onI)
+qed (auto intro: antimono_imp_strict_antimono)
+
 lemma mono_compose: "mono Q \<Longrightarrow> mono (\<lambda>i x. Q i (f x))"
   unfolding mono_def le_fun_def by auto
 
diff -r 0649ff183dcf -r 01c88cf514fc src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue May 02 11:09:18 2023 +0100
+++ b/src/HOL/Real.thy	Tue May 02 12:51:05 2023 +0100
@@ -1096,6 +1096,27 @@
   by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc)
 
 
+lemma inverse_Suc: "inverse (Suc n) > 0"
+  using of_nat_0_less_iff positive_imp_inverse_positive zero_less_Suc by blast
+
+lemma Archimedean_eventually_inverse:
+  fixes \<epsilon>::real shows "(\<forall>\<^sub>F n in sequentially. inverse (real (Suc n)) < \<epsilon>) \<longleftrightarrow> 0 < \<epsilon>"
+  (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    unfolding eventually_at_top_dense using inverse_Suc order_less_trans by blast
+next
+  assume ?rhs
+  then obtain N where "inverse (Suc N) < \<epsilon>"
+    using reals_Archimedean by blast
+  moreover have "inverse (Suc n) \<le> inverse (Suc N)" if "n \<ge> N" for n
+    using inverse_Suc that by fastforce
+  ultimately show ?lhs
+    unfolding eventually_sequentially
+    using order_le_less_trans by blast
+qed
+
 subsection \<open>Rationals\<close>
 
 lemma Rats_abs_iff[simp]: