# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1524063456 -3600
# Node ID 1b05f74f2e5f8948de6f50ab8d6020fdc601debf
# Parent  73a5a33486ee2400ee0701d632dee57af52864c3
tidying up including contributions from Paulo Emílio de Vilhena

diff -r 73a5a33486ee -r 1b05f74f2e5f NEWS
--- a/NEWS	Tue Apr 17 22:35:48 2018 +0100
+++ b/NEWS	Wed Apr 18 15:57:36 2018 +0100
@@ -209,6 +209,10 @@
 choice operator. The dual of this property is also proved in 
 Hilbert_Choice.thy.
 
+* New syntax for the minimum/maximum of a function over a finite set:
+MIN x\<in>A. B  and even  MIN x. B (only useful for finite types), also
+MAX.
+
 * Clarifed theorem names:
 
   Min.antimono ~> Min.subset_imp
@@ -255,8 +259,9 @@
 
 * HOL-Algebra: renamed (^) to [^]
 
-* Session HOL-Analysis: Moebius functions and the Riemann mapping
-theorem.
+* Session HOL-Analysis: Moebius functions, the Riemann mapping
+theorem, the Vitali covering theorem, change-of-variables results for
+integration and measures.
 
 * Class linordered_semiring_1 covers zero_less_one also, ruling out
 pathologic instances. Minor INCOMPATIBILITY.
diff -r 73a5a33486ee -r 1b05f74f2e5f src/HOL/Algebra/Congruence.thy
--- a/src/HOL/Algebra/Congruence.thy	Tue Apr 17 22:35:48 2018 +0100
+++ b/src/HOL/Algebra/Congruence.thy	Wed Apr 18 15:57:36 2018 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Algebra/Congruence.thy
     Author:     Clemens Ballarin, started 3 January 2008
-    Copyright:  Clemens Ballarin
+    with thanks to Paulo Emílio de Vilhena
 *)
 
 theory Congruence
@@ -119,7 +119,7 @@
 by (fast intro: elemI elim: elemE dest: subsetD)
 
 lemma (in equivalence) mem_imp_elem [simp, intro]:
-  "[| x \<in> A; x \<in> carrier S |] ==> x .\<in> A"
+  "\<lbrakk> x \<in> A; x \<in> carrier S \<rbrakk> \<Longrightarrow> x .\<in> A"
   unfolding elem_def by blast
 
 lemma set_eqI:
@@ -215,15 +215,11 @@
 
 lemma (in equivalence) set_eq_sym [sym]:
   assumes "A {.=} B"
-    and "A \<subseteq> carrier S" "B \<subseteq> carrier S"
   shows "B {.=} A"
 using assms
 unfolding set_eq_def elem_def
 by fast
 
-(* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *)
-(* alternatively, could declare lemmas [trans] = ssubst [where 'a = "'a set"] *)
-
 lemma (in equivalence) equal_set_eq_trans [trans]:
   assumes AB: "A = B" and BC: "B {.=} C"
   shows "A {.=} C"
@@ -234,7 +230,6 @@
   shows "A {.=} C"
   using AB BC by simp
 
-
 lemma (in equivalence) set_eq_trans [trans]:
   assumes AB: "A {.=} B" and BC: "B {.=} C"
     and carr: "A \<subseteq> carrier S"  "B \<subseteq> carrier S"  "C \<subseteq> carrier S"
@@ -265,46 +260,46 @@
        show "c .\<in> A" by simp
 qed
 
-(* FIXME: generalise for insert *)
+lemma (in equivalence) set_eq_insert_aux:
+  assumes x: "x .= x'"
+      and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S"
+    shows "\<forall>a \<in> (insert x A). a .\<in> (insert x' A)"
+proof
+  fix a
+  show "a \<in> insert x A \<Longrightarrow> a .\<in> insert x' A"
+  proof cases
+    assume "a \<in> A"
+    thus "a .\<in> insert x' A"
+      using carr(3) by blast
+  next
+    assume "a \<in> insert x A" "a \<notin> A"
+    hence "a = x"
+      by blast
+    thus "a .\<in> insert x' A"
+      by (meson x elemI insertI1)
+  qed
+qed
 
-(*
 lemma (in equivalence) set_eq_insert:
   assumes x: "x .= x'"
-    and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S"
-  shows "insert x A {.=} insert x' A"
-  unfolding set_eq_def elem_def
-apply rule
-apply rule
-apply (case_tac "xa = x")
-using x apply fast
-apply (subgoal_tac "xa \<in> A") prefer 2 apply fast
-apply (rule_tac x=xa in bexI)
-using carr apply (rule_tac refl) apply auto [1]
-apply safe
-*)
+      and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S"
+    shows "insert x A {.=} insert x' A"
+proof-
+  have "(\<forall>a \<in> (insert x  A). a .\<in> (insert x' A)) \<and>
+        (\<forall>a \<in> (insert x' A). a .\<in> (insert x  A))"
+    using set_eq_insert_aux carr x sym by blast
+  thus "insert x A {.=} insert x' A"
+    using set_eq_def by blast
+qed  
 
 lemma (in equivalence) set_eq_pairI:
   assumes xx': "x .= x'"
     and carr: "x \<in> carrier S" "x' \<in> carrier S" "y \<in> carrier S"
   shows "{x, y} {.=} {x', y}"
-unfolding set_eq_def elem_def
-proof safe
-  have "x' \<in> {x', y}" by fast
-  with xx' show "\<exists>b\<in>{x', y}. x .= b" by fast
-next
-  have "y \<in> {x', y}" by fast
-  with carr show "\<exists>b\<in>{x', y}. y .= b" by fast
-next
-  have "x \<in> {x, y}" by fast
-  with xx'[symmetric] carr
-  show "\<exists>a\<in>{x, y}. x' .= a" by fast
-next
-  have "y \<in> {x, y}" by fast
-  with carr show "\<exists>a\<in>{x, y}. y .= a" by fast
-qed
+  using assms set_eq_insert by simp
 
 lemma (in equivalence) is_closedI:
-  assumes closed: "!!x y. [| x .= y; x \<in> A; y \<in> carrier S |] ==> y \<in> A"
+  assumes closed: "\<And>x y. \<lbrakk>x .= y; x \<in> A; y \<in> carrier S\<rbrakk> \<Longrightarrow> y \<in> A"
     and S: "A \<subseteq> carrier S"
   shows "is_closed A"
   unfolding eq_is_closed_def eq_closure_of_def elem_def
@@ -312,19 +307,19 @@
   by (blast dest: closed sym)
 
 lemma (in equivalence) closure_of_eq:
-  "[| x .= x'; A \<subseteq> carrier S; x \<in> closure_of A; x \<in> carrier S; x' \<in> carrier S |] ==> x' \<in> closure_of A"
+  "\<lbrakk>x .= x'; A \<subseteq> carrier S; x \<in> closure_of A; x' \<in> carrier S\<rbrakk> \<Longrightarrow> x' \<in> closure_of A"
   unfolding eq_closure_of_def elem_def
   by (blast intro: trans sym)
 
 lemma (in equivalence) is_closed_eq [dest]:
-  "[| x .= x'; x \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S |] ==> x' \<in> A"
+  "\<lbrakk>x .= x'; x \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S\<rbrakk> \<Longrightarrow> x' \<in> A"
   unfolding eq_is_closed_def
   using closure_of_eq [where A = A]
   by simp
 
 lemma (in equivalence) is_closed_eq_rev [dest]:
-  "[| x .= x'; x' \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S |] ==> x \<in> A"
-  by (drule sym) (simp_all add: is_closed_eq)
+  "\<lbrakk>x .= x'; x' \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S\<rbrakk> \<Longrightarrow> x \<in> A"
+  by (meson subsetD eq_is_closed_def is_closed_eq sym)
 
 lemma closure_of_closed [simp, intro]:
   fixes S (structure)
@@ -334,81 +329,55 @@
 
 lemma closure_of_memI:
   fixes S (structure)
-  assumes "a .\<in> A"
-    and "a \<in> carrier S"
+  assumes "a .\<in> A" and "a \<in> carrier S"
   shows "a \<in> closure_of A"
-unfolding eq_closure_of_def
-using assms
-by fast
+  by (simp add: assms eq_closure_of_def)
 
 lemma closure_ofI2:
   fixes S (structure)
-  assumes "a .= a'"
-    and "a' \<in> A"
-    and "a \<in> carrier S"
+  assumes "a .= a'" and "a' \<in> A" and "a \<in> carrier S"
   shows "a \<in> closure_of A"
-unfolding eq_closure_of_def elem_def
-using assms
-by fast
+  by (meson assms closure_of_memI elem_def)
 
 lemma closure_of_memE:
   fixes S (structure)
-  assumes p: "a \<in> closure_of A"
-    and r: "\<lbrakk>a \<in> carrier S; a .\<in> A\<rbrakk> \<Longrightarrow> P"
+  assumes "a \<in> closure_of A"
+    and "\<lbrakk>a \<in> carrier S; a .\<in> A\<rbrakk> \<Longrightarrow> P"
   shows "P"
-proof -
-  from p
-      have acarr: "a \<in> carrier S"
-      and "a .\<in> A"
-      by (simp add: eq_closure_of_def)+
-  thus "P" by (rule r)
-qed
+  using eq_closure_of_def assms by fastforce
 
 lemma closure_ofE2:
   fixes S (structure)
-  assumes p: "a \<in> closure_of A"
-    and r: "\<And>a'. \<lbrakk>a \<in> carrier S; a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
+  assumes "a \<in> closure_of A"
+    and "\<And>a'. \<lbrakk>a \<in> carrier S; a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
   shows "P"
-proof -
-  from p have acarr: "a \<in> carrier S" by (simp add: eq_closure_of_def)
+  by (meson closure_of_memE elemE assms)
 
-  from p have "\<exists>a'\<in>A. a .= a'" by (simp add: eq_closure_of_def elem_def)
-  from this obtain a'
-      where "a' \<in> A" and "a .= a'" by auto
-
-  from acarr and this
-      show "P" by (rule r)
+lemma (in equivalence) closure_inclusion:
+  assumes "A \<subseteq> B"
+  shows "closure_of A \<subseteq> closure_of B"
+  unfolding eq_closure_of_def
+proof
+  fix x
+  assume "x \<in> {y \<in> carrier S. y .\<in> A}"
+  hence "x \<in> carrier S \<and> x .\<in> A"
+    by blast
+  hence "x \<in> carrier S \<and> x .\<in> B"
+    using assms elem_subsetD by blast
+  thus "x \<in> {y \<in> carrier S. y .\<in> B}"
+    by simp
 qed
 
-(*
-lemma (in equivalence) classes_consistent:
-  assumes Acarr: "A \<subseteq> carrier S"
-  shows "is_closed (closure_of A)"
-apply (blast intro: elemI elim elemE)
-using assms
-apply (intro is_closedI closure_of_memI, simp)
- apply (elim elemE closure_of_memE)
-proof -
-  fix x a' a''
-  assume carr: "x \<in> carrier S" "a' \<in> carrier S"
-  assume a''A: "a'' \<in> A"
-  with Acarr have "a'' \<in> carrier S" by fast
-  note [simp] = carr this Acarr
-
-  assume "x .= a'"
-  also assume "a' .= a''"
-  also from a''A
-       have "a'' .\<in> A" by (simp add: elem_exact)
-  finally show "x .\<in> A" by simp
-qed
-*)
-(*
 lemma (in equivalence) classes_small:
   assumes "is_closed B"
     and "A \<subseteq> B"
   shows "closure_of A \<subseteq> B"
-using assms
-by (blast dest: is_closedD2 elem_subsetD elim: closure_of_memE)
+proof-
+  have "closure_of A \<subseteq> closure_of B"
+    using closure_inclusion assms by simp
+  thus "closure_of A \<subseteq> B"
+    using assms(1) eq_is_closed_def by fastforce
+qed
 
 lemma (in equivalence) classes_eq:
   assumes "A \<subseteq> carrier S"
@@ -419,9 +388,21 @@
 lemma (in equivalence) complete_classes:
   assumes c: "is_closed A"
   shows "A = closure_of A"
-using assms
-by (blast intro: closure_of_memI elem_exact dest: is_closedD1 is_closedD2 closure_of_memE)
-*)
+  using assms by (simp add: eq_is_closed_def)
+
+lemma (in equivalence) closure_idemp_weak:
+  "closure_of (closure_of A) {.=} closure_of A"
+  by (simp add: classes_eq set_eq_sym)
+
+lemma (in equivalence) closure_idemp_strong:
+  assumes "A \<subseteq> carrier S"
+  shows "closure_of (closure_of A) = closure_of A"
+  using assms closure_of_eq complete_classes is_closedI by auto
+
+lemma (in equivalence) complete_classes2:
+  assumes "A \<subseteq> carrier S"
+  shows "is_closed (closure_of A)"
+  using closure_idemp_strong by (simp add: assms eq_is_closed_def)
 
 lemma equivalence_subset:
   assumes "equivalence L" "A \<subseteq> carrier L"
diff -r 73a5a33486ee -r 1b05f74f2e5f src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Tue Apr 17 22:35:48 2018 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Wed Apr 18 15:57:36 2018 +0100
@@ -1,12 +1,12 @@
 theory Change_Of_Vars
-  imports  "HOL-Analysis.Vitali_Covering_Theorem" "HOL-Analysis.Determinants"
+  imports Vitali_Covering_Theorem Determinants
 
 begin
 
 subsection\<open>Induction on matrix row operations\<close>
 
 lemma induct_matrix_row_operations:
-  fixes P :: "(real^'n, 'n::finite) vec \<Rightarrow> bool"
+  fixes P :: "real^'n^'n \<Rightarrow> bool"
   assumes zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
     and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
     and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A $ i $ Fun.swap m n id j)"
@@ -115,7 +115,7 @@
 qed
 
 lemma induct_matrix_elementary:
-  fixes P :: "(real^'n, 'n::finite) vec \<Rightarrow> bool"
+  fixes P :: "real^'n^'n \<Rightarrow> bool"
   assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
     and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
     and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
@@ -146,7 +146,7 @@
 qed
 
 lemma induct_matrix_elementary_alt:
-  fixes P :: "(real^'n, 'n::finite) vec \<Rightarrow> bool"
+  fixes P :: "real^'n^'n \<Rightarrow> bool"
   assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
     and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
     and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
@@ -196,14 +196,14 @@
     then show "P (( *v) (A ** B))"
       by (metis (no_types, lifting) comp linear_compose matrix_compose matrix_eq matrix_vector_mul matrix_vector_mul_linear)
   next
-    fix A :: "((real, 'n) vec, 'n) vec" and i
+    fix A :: "real^'n^'n" and i
     assume "row i A = 0"
     then show "P (( *v) A)"
       by (metis inner_zero_left matrix_vector_mul_component matrix_vector_mul_linear row_def vec_eq_iff vec_lambda_beta zeroes)
   next
-    fix A :: "((real, 'n) vec, 'n) vec"
+    fix A :: "real^'n^'n"
     assume 0: "\<And>i j. i \<noteq> j \<Longrightarrow> A $ i $ j = 0"
-    have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x :: "(real, 'n) vec" and i :: "'n"
+    have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x and i :: "'n"
       by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i])
     then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = (( *v) A)"
       by (auto simp: 0 matrix_vector_mult_def)
@@ -214,7 +214,7 @@
     assume "m \<noteq> n"
     have eq: "(\<Sum>j\<in>UNIV. if i = Fun.swap m n id j then x $ j else 0) =
               (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
-      for i and x :: "(real, 'n) vec"
+      for i and x :: "real^'n"
       unfolding swap_def by (rule sum.cong) auto
     have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = (( *v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
       by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
@@ -223,7 +223,7 @@
   next
     fix m n :: "'n"
     assume "m \<noteq> n"
-    then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "(real, 'n) vec"
+    then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "real^'n"
       by (auto simp: of_bool_def if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
     then have "(\<lambda>x::real^'n. \<chi> i. if i = m then x $ m + x $ n else x $ i) =
                (( *v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
@@ -390,7 +390,7 @@
             using True by auto
           have "ball 0 B \<subseteq> (\<lambda>x. \<chi> k. x $ k / m k) ` ball 0 ?C"
           proof clarsimp
-            fix x :: "(real, 'n) vec"
+            fix x :: "real^'n"
             assume x: "norm x < B"
             have [simp]: "\<bar>Max (range (\<lambda>k. \<bar>m k\<bar>))\<bar> = Max (range (\<lambda>k. \<bar>m k\<bar>))"
               by (meson Max_ge abs_ge_zero abs_of_nonneg finite finite_imageI order_trans rangeI)
@@ -452,8 +452,6 @@
 
 
 
-
-
 proposition
  fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
   assumes "linear f" "S \<in> lmeasurable"
@@ -473,7 +471,7 @@
       using f [OF gS] g [OF S] matrix_compose [OF \<open>linear g\<close> \<open>linear f\<close>]
       by (simp add: o_def image_comp abs_mult det_mul)
   next
-    fix f :: "(real, 'n) vec \<Rightarrow> (real, 'n) vec" and i and S :: "(real, 'n) vec set"
+    fix f :: "real^'n::_ \<Rightarrow> real^'n::_" and i and S :: "(real^'n::_) set"
     assume "linear f" and 0: "\<And>x. f x $ i = 0" and "S \<in> lmeasurable"
     then have "\<not> inj f"
       by (metis (full_types) linear_injective_imp_surjective one_neq_zero surjE vec_component)
@@ -490,7 +488,7 @@
       finally show "?Q f S" .
     qed
   next
-    fix c and S :: "(real, 'n) vec set"
+    fix c and S :: "(real^'n::_) set"
     assume "S \<in> lmeasurable"
     show "(\<lambda>a. \<chi> i. c i * a $ i) ` S \<in> lmeasurable \<and> ?Q (\<lambda>a. \<chi> i. c i * a $ i) S"
     proof
@@ -532,7 +530,7 @@
         using measure_linear_sufficient [OF lin \<open>S \<in> lmeasurable\<close>] meq 1 by force+
     qed
   next
-    fix m :: "'n" and n :: "'n" and S :: "(real, 'n) vec set"
+    fix m n :: "'n" and S :: "(real, 'n) vec set"
     assume "m \<noteq> n" and "S \<in> lmeasurable"
     let ?h = "\<lambda>v::(real, 'n) vec. \<chi> i. if i = m then v $ m + v $ n else v $ i"
     have lin: "linear ?h"
@@ -616,26 +614,6 @@
     by (simp add: measure_linear_image \<open>linear f\<close> S f)
 qed
 
-lemma sets_lebesgue_inner_closed:
-  assumes "S \<in> sets lebesgue" "e > 0"
-  obtains T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "measure lebesgue (S - T) < e"
-proof -
-  have "-S \<in> sets lebesgue"
-    using assms by (simp add: Compl_in_sets_lebesgue)
-  then obtain T where "open T" "-S \<subseteq> T"
-          and T: "(T - -S) \<in> lmeasurable" "measure lebesgue (T - -S) < e"
-    using lmeasurable_outer_open assms  by blast
-  show thesis
-  proof
-    show "closed (-T)"
-      using \<open>open T\<close> by blast
-    show "-T \<subseteq> S"
-      using \<open>- S \<subseteq> T\<close> by auto
-    show "S - ( -T) \<in> lmeasurable" "measure lebesgue (S - (- T)) < e"
-      using T by (auto simp: Int_commute)
-  qed
-qed
-
 subsection\<open>@{text F_sigma} and @{text G_delta} sets.\<close>
 
 (*https://en.wikipedia.org/wiki/F\<sigma>_set*)
@@ -645,7 +623,6 @@
 inductive gdelta :: "'a::topological_space set \<Rightarrow> bool" where
   "(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (INTER UNIV F)"
 
-
 lemma fsigma_Union_compact:
   fixes S :: "'a::{real_normed_vector,heine_borel} set"
   shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = UNION UNIV F)"
@@ -698,12 +675,9 @@
     by (simp add: 1 gdelta.intros open_closed)
 qed
 
-
-
 lemma gdelta_complement: "gdelta(- S) \<longleftrightarrow> fsigma S"
   using fsigma_imp_gdelta gdelta_imp_fsigma by force
 
-
 text\<open>A Lebesgue set is almost an @{text F_sigma} or @{text G_delta}.\<close>
 lemma lebesgue_set_almost_fsigma:
   assumes "S \<in> sets lebesgue"
@@ -1839,7 +1813,7 @@
           using \<open>r > 0\<close> \<open>d > 0\<close> by auto
         show "{x' \<in> S. \<exists>v. v \<noteq> 0 \<and> (\<forall>\<xi>>0. \<exists>e>0. \<forall>z\<in>S - {x'}. norm (x' - z) < e \<longrightarrow> \<bar>v \<bullet> (z - x')\<bar> < \<xi> * norm (x' - z))} \<inter> ball x (min d r) \<subseteq> ?W"
           proof (clarsimp simp: dist_norm norm_minus_commute)
-            fix y :: "(real, 'm) vec" and w :: "(real, 'm) vec"
+            fix y w 
             assume "y \<in> S" "w \<noteq> 0"
               and less [rule_format]:
                     "\<forall>\<xi>>0. \<exists>e>0. \<forall>z\<in>S - {y}. norm (y - z) < e \<longrightarrow> \<bar>w \<bullet> (z - y)\<bar> < \<xi> * norm (y - z)"
diff -r 73a5a33486ee -r 1b05f74f2e5f src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Tue Apr 17 22:35:48 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Apr 18 15:57:36 2018 +0100
@@ -1297,6 +1297,26 @@
   qed
 qed
 
+lemma sets_lebesgue_inner_closed:
+  assumes "S \<in> sets lebesgue" "e > 0"
+  obtains T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "measure lebesgue (S - T) < e"
+proof -
+  have "-S \<in> sets lebesgue"
+    using assms by (simp add: Compl_in_sets_lebesgue)
+  then obtain T where "open T" "-S \<subseteq> T"
+          and T: "(T - -S) \<in> lmeasurable" "measure lebesgue (T - -S) < e"
+    using lmeasurable_outer_open assms  by blast
+  show thesis
+  proof
+    show "closed (-T)"
+      using \<open>open T\<close> by blast
+    show "-T \<subseteq> S"
+      using \<open>- S \<subseteq> T\<close> by auto
+    show "S - ( -T) \<in> lmeasurable" "measure lebesgue (S - (- T)) < e"
+      using T by (auto simp: Int_commute)
+  qed
+qed
+
 lemma lebesgue_openin:
    "\<lbrakk>openin (subtopology euclidean S) T; S \<in> sets lebesgue\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
   by (metis borel_open openin_open sets.Int sets_completionI_sets sets_lborel)