three new theorems
authorpaulson <lp15@cam.ac.uk>
Fri Apr 20 19:11:17 2018 +0100 (16 months ago)
changeset 68017e99f9b3962bf
parent 68016 5eb4081e6bf6
child 68019 32d19862781b
three new theorems
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Change_Of_Vars.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Vitali_Covering_Theorem.thy
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Apr 20 15:58:02 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Apr 20 19:11:17 2018 +0100
     1.3 @@ -5291,4 +5291,16 @@
     1.4    using connected_complement_homeomorphic_convex_compact [OF assms]
     1.5    using \<open>compact T\<close> compact_eq_bounded_closed connected_open_path_connected hom homeomorphic_compactness by blast
     1.6  
     1.7 +lemma path_connected_complement_homeomorphic_interval:
     1.8 +  fixes S :: "'a::euclidean_space set"
     1.9 +  assumes "S homeomorphic cbox a b" "2 \<le> DIM('a)"
    1.10 +  shows "path_connected(-S)"
    1.11 +  using assms compact_cbox convex_box(1) path_connected_complement_homeomorphic_convex_compact by blast
    1.12 +
    1.13 +lemma connected_complement_homeomorphic_interval:
    1.14 +  fixes S :: "'a::euclidean_space set"
    1.15 +  assumes "S homeomorphic cbox a b" "2 \<le> DIM('a)"
    1.16 +  shows "connected(-S)"
    1.17 +  using assms path_connected_complement_homeomorphic_interval path_connected_imp_connected by blast
    1.18 +
    1.19  end
     2.1 --- a/src/HOL/Analysis/Change_Of_Vars.thy	Fri Apr 20 15:58:02 2018 +0200
     2.2 +++ b/src/HOL/Analysis/Change_Of_Vars.thy	Fri Apr 20 19:11:17 2018 +0100
     2.3 @@ -1,3 +1,9 @@
     2.4 +(*  Title:      HOL/Analysis/Change_Of_Vars.thy
     2.5 +    Authors:    LC Paulson, based on material from HOL Light
     2.6 +*)
     2.7 +
     2.8 +section\<open>Change of Variables Theorems\<close>
     2.9 +
    2.10  theory Change_Of_Vars
    2.11    imports Vitali_Covering_Theorem Determinants
    2.12  
     3.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Apr 20 15:58:02 2018 +0200
     3.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Apr 20 19:11:17 2018 +0100
     3.3 @@ -1325,6 +1325,13 @@
     3.4      by (simp add: negligible_interval box_eq_empty algebra_simps divide_simps mult_le_0_iff)
     3.5  qed
     3.6  
     3.7 +lemma negligible_convex_interior:
     3.8 +   "convex S \<Longrightarrow> (negligible S \<longleftrightarrow> interior S = {})"
     3.9 +  apply safe
    3.10 +  apply (metis interior_subset negligible_subset open_interior open_not_negligible)
    3.11 +   apply (metis Diff_empty closure_subset frontier_def negligible_convex_frontier negligible_subset)
    3.12 +  done
    3.13 +
    3.14  lemma measure_eq_0_null_sets: "S \<in> null_sets M \<Longrightarrow> measure M S = 0"
    3.15    by (auto simp: measure_def null_sets_def)
    3.16  
     4.1 --- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Fri Apr 20 15:58:02 2018 +0200
     4.2 +++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Fri Apr 20 19:11:17 2018 +0100
     4.3 @@ -1,3 +1,9 @@
     4.4 +(*  Title:      HOL/Analysis/Vitali_Covering_Theorem.thy
     4.5 +    Authors:    LC Paulson, based on material from HOL Light
     4.6 +*)
     4.7 +
     4.8 +section\<open>Vitali Covering Theorem and an Application to Negligibility\<close>
     4.9 +
    4.10  theory Vitali_Covering_Theorem
    4.11    imports Ball_Volume "HOL-Library.Permutations"
    4.12