--- 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)
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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]: