--- a/src/HOL/Analysis/Borel_Space.thy Tue Aug 27 22:31:21 2019 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy Tue Aug 27 22:41:47 2019 +0200
@@ -221,29 +221,6 @@
apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def)
using assms differentiable_at_withinI real_differentiable_def by blast
-lemma closure_contains_Sup:
- fixes S :: "real set"
- assumes "S \<noteq> {}" "bdd_above S"
- shows "Sup S \<in> closure S"
-proof -
- have "Inf (uminus ` S) \<in> closure (uminus ` S)"
- using assms by (intro closure_contains_Inf) auto
- also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def image_comp)
- also have "closure (uminus ` S) = uminus ` closure S"
- by (rule sym, intro closure_injective_linear_image) (auto intro: linearI)
- finally show ?thesis by auto
-qed
-
-lemma closed_contains_Sup:
- fixes S :: "real set"
- shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
- by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
-
-lemma closed_subset_contains_Sup:
- fixes A C :: "real set"
- shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> Sup A \<in> C"
- by (metis closure_contains_Sup closure_minimal subset_eq)
-
lemma continuous_interval_vimage_Int:
assumes "continuous_on {a::real..b} g" and mono: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
assumes "a \<le> b" "(c::real) \<le> d" "{c..d} \<subseteq> {g a..g b}"
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Aug 27 22:31:21 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Aug 27 22:41:47 2019 +0200
@@ -677,6 +677,25 @@
then show ?thesis unfolding closure_approachable by auto
qed
+lemma closure_contains_Sup:
+ fixes S :: "real set"
+ assumes "S \<noteq> {}" "bdd_above S"
+ shows "Sup S \<in> closure S"
+proof -
+ have *: "\<forall>x\<in>S. x \<le> Sup S"
+ using cSup_upper[of _ S] assms by metis
+ {
+ fix e :: real
+ assume "e > 0"
+ then have "Sup S - e < Sup S" by simp
+ with assms obtain x where "x \<in> S" "Sup S - e < x"
+ by (subst (asm) less_cSup_iff) auto
+ with * have "\<exists>x\<in>S. dist x (Sup S) < e"
+ by (intro bexI[of _ x]) (auto simp: dist_real_def)
+ }
+ then show ?thesis unfolding closure_approachable by auto
+qed
+
lemma not_trivial_limit_within_ball:
"\<not> trivial_limit (at x within S) \<longleftrightarrow> (\<forall>e>0. S \<inter> ball x e - {x} \<noteq> {})"
(is "?lhs \<longleftrightarrow> ?rhs")
@@ -2922,6 +2941,16 @@
shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> Inf A \<in> C"
by (metis closure_contains_Inf closure_minimal subset_eq)
+lemma closed_contains_Sup:
+ fixes S :: "real set"
+ shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
+ by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
+
+lemma closed_subset_contains_Sup:
+ fixes A C :: "real set"
+ shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> Sup A \<in> C"
+ by (metis closure_contains_Sup closure_minimal subset_eq)
+
lemma atLeastAtMost_subset_contains_Inf:
fixes A :: "real set" and a b :: real
shows "A \<noteq> {} \<Longrightarrow> a \<le> b \<Longrightarrow> A \<subseteq> {a..b} \<Longrightarrow> Inf A \<in> {a..b}"
--- a/src/HOL/Analysis/Lipschitz.thy Tue Aug 27 22:31:21 2019 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy Tue Aug 27 22:41:47 2019 +0200
@@ -5,7 +5,8 @@
section \<open>Lipschitz Continuity\<close>
theory Lipschitz
-imports Borel_Space
+ imports
+ Derivative
begin
definition\<^marker>\<open>tag important\<close> lipschitz_on