# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1524247877 -3600
# Node ID e99f9b3962bf17122d9d7b945fe5c07a2e3aa297
# Parent  5eb4081e6bf6cea52e03467b8b94b37f9a5c18b9
three new theorems

diff -r 5eb4081e6bf6 -r e99f9b3962bf src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Apr 20 15:58:02 2018 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Apr 20 19:11:17 2018 +0100
@@ -5291,4 +5291,16 @@
   using connected_complement_homeomorphic_convex_compact [OF assms]
   using \<open>compact T\<close> compact_eq_bounded_closed connected_open_path_connected hom homeomorphic_compactness by blast
 
+lemma path_connected_complement_homeomorphic_interval:
+  fixes S :: "'a::euclidean_space set"
+  assumes "S homeomorphic cbox a b" "2 \<le> DIM('a)"
+  shows "path_connected(-S)"
+  using assms compact_cbox convex_box(1) path_connected_complement_homeomorphic_convex_compact by blast
+
+lemma connected_complement_homeomorphic_interval:
+  fixes S :: "'a::euclidean_space set"
+  assumes "S homeomorphic cbox a b" "2 \<le> DIM('a)"
+  shows "connected(-S)"
+  using assms path_connected_complement_homeomorphic_interval path_connected_imp_connected by blast
+
 end
diff -r 5eb4081e6bf6 -r e99f9b3962bf src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Fri Apr 20 15:58:02 2018 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Fri Apr 20 19:11:17 2018 +0100
@@ -1,3 +1,9 @@
+(*  Title:      HOL/Analysis/Change_Of_Vars.thy
+    Authors:    LC Paulson, based on material from HOL Light
+*)
+
+section\<open>Change of Variables Theorems\<close>
+
 theory Change_Of_Vars
   imports Vitali_Covering_Theorem Determinants
 
diff -r 5eb4081e6bf6 -r e99f9b3962bf src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Apr 20 15:58:02 2018 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Apr 20 19:11:17 2018 +0100
@@ -1325,6 +1325,13 @@
     by (simp add: negligible_interval box_eq_empty algebra_simps divide_simps mult_le_0_iff)
 qed
 
+lemma negligible_convex_interior:
+   "convex S \<Longrightarrow> (negligible S \<longleftrightarrow> interior S = {})"
+  apply safe
+  apply (metis interior_subset negligible_subset open_interior open_not_negligible)
+   apply (metis Diff_empty closure_subset frontier_def negligible_convex_frontier negligible_subset)
+  done
+
 lemma measure_eq_0_null_sets: "S \<in> null_sets M \<Longrightarrow> measure M S = 0"
   by (auto simp: measure_def null_sets_def)
 
diff -r 5eb4081e6bf6 -r e99f9b3962bf src/HOL/Analysis/Vitali_Covering_Theorem.thy
--- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Fri Apr 20 15:58:02 2018 +0200
+++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Fri Apr 20 19:11:17 2018 +0100
@@ -1,3 +1,9 @@
+(*  Title:      HOL/Analysis/Vitali_Covering_Theorem.thy
+    Authors:    LC Paulson, based on material from HOL Light
+*)
+
+section\<open>Vitali Covering Theorem and an Application to Negligibility\<close>
+
 theory Vitali_Covering_Theorem
   imports Ball_Volume "HOL-Library.Permutations"