# HG changeset patch
# User immler
# Date 1566938507 -7200
# Node ID c81ac117afa642cc3f24271ee3f51ed3900a7e6c
# Parent  6bc397bc8e8a780c51d24d552196f4095112e334
moved lemmas; reduced dependencies of Lipschitz

diff -r 6bc397bc8e8a -r c81ac117afa6 src/HOL/Analysis/Borel_Space.thy
--- 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}"
diff -r 6bc397bc8e8a -r c81ac117afa6 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- 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}"
diff -r 6bc397bc8e8a -r c81ac117afa6 src/HOL/Analysis/Lipschitz.thy
--- 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