diff -r c06604896c3d -r c213d067e60f src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Tue Feb 25 17:37:22 2020 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy	Wed Feb 26 12:21:48 2020 +0000
@@ -28,78 +28,6 @@
     by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis)
 qed
 
-definition\<^marker>\<open>tag important\<close> "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s"
-
-lemma mono_onI:
-  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on f A"
-  unfolding mono_on_def by simp
-
-lemma mono_onD:
-  "\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
-  unfolding mono_on_def by simp
-
-lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A"
-  unfolding mono_def mono_on_def by auto
-
-lemma mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B"
-  unfolding mono_on_def by auto
-
-definition\<^marker>\<open>tag important\<close> "strict_mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s"
-
-lemma strict_mono_onI:
-  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on f A"
-  unfolding strict_mono_on_def by simp
-
-lemma strict_mono_onD:
-  "\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
-  unfolding strict_mono_on_def by simp
-
-lemma mono_on_greaterD:
-  assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
-  shows "x > y"
-proof (rule ccontr)
-  assume "\<not>x > y"
-  hence "x \<le> y" by (simp add: not_less)
-  from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD)
-  with assms(4) show False by simp
-qed
-
-lemma strict_mono_inv:
-  fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)"
-  assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x"
-  shows "strict_mono g"
-proof
-  fix x y :: 'b assume "x < y"
-  from \<open>surj f\<close> obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast
-  with \<open>x < y\<close> and \<open>strict_mono f\<close> have "x' < y'" by (simp add: strict_mono_less)
-  with inv show "g x < g y" by simp
-qed
-
-lemma strict_mono_on_imp_inj_on:
-  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A"
-  shows "inj_on f A"
-proof (rule inj_onI)
-  fix x y assume "x \<in> A" "y \<in> A" "f x = f y"
-  thus "x = y"
-    by (cases x y rule: linorder_cases)
-       (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x])
-qed
-
-lemma strict_mono_on_leD:
-  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y"
-  shows "f x \<le> f y"
-proof (insert le_less_linear[of y x], elim disjE)
-  assume "x < y"
-  with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all
-  thus ?thesis by (rule less_imp_le)
-qed (insert assms, simp)
-
-lemma strict_mono_on_eqD:
-  fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)"
-  assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A"
-  shows "y = x"
-  using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD)
-
 proposition mono_on_imp_deriv_nonneg:
   assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
   assumes "x \<in> interior A"
@@ -127,10 +55,6 @@
   qed
 qed simp
 
-lemma strict_mono_on_imp_mono_on:
-  "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A"
-  by (rule mono_onI, rule strict_mono_on_leD)
-
 proposition mono_on_ctble_discont:
   fixes f :: "real \<Rightarrow> real"
   fixes A :: "real set"