# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1635331662 -3600
# Node ID 5d91897a8e5420fdd824b6b64cd2fde2d469e7bc
# Parent  ea5d28c7f5e57ecf3f368e3179c8f8c6938f7f17
moved a theorem to a sensible place

diff -r ea5d28c7f5e5 -r 5d91897a8e54 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Tue Oct 26 22:58:20 2021 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Wed Oct 27 11:47:42 2021 +0100
@@ -1602,10 +1602,6 @@
     measure M (A \<union> B) = measure M A + measure M B"
   by (simp add: measure_def plus_emeasure[symmetric] enn2real_plus less_top)
 
-lemma disjoint_family_on_insert:
-  "i \<notin> I \<Longrightarrow> disjoint_family_on A (insert i I) \<longleftrightarrow> A i \<inter> (\<Union>i\<in>I. A i) = {} \<and> disjoint_family_on A I"
-  by (fastforce simp: disjoint_family_on_def)
-
 lemma measure_finite_Union:
   "finite S \<Longrightarrow> A`S \<subseteq> sets M \<Longrightarrow> disjoint_family_on A S \<Longrightarrow> (\<And>i. i \<in> S \<Longrightarrow> emeasure M (A i) \<noteq> \<infinity>) \<Longrightarrow>
     measure M (\<Union>i\<in>S. A i) = (\<Sum>i\<in>S. measure M (A i))"
@@ -2400,7 +2396,7 @@
       then have "infinite (\<Union>i. F i)"
         by auto
       ultimately show ?thesis by (simp only:) simp
-         
+
     qed
   qed
 qed
diff -r ea5d28c7f5e5 -r 5d91897a8e54 src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Tue Oct 26 22:58:20 2021 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy	Wed Oct 27 11:47:42 2021 +0100
@@ -122,6 +122,10 @@
 lemma disjoint_family_subset: "disjoint_family A \<Longrightarrow> (\<And>x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
   by (force simp add: disjoint_family_on_def)
 
+lemma disjoint_family_on_insert:
+  "i \<notin> I \<Longrightarrow> disjoint_family_on A (insert i I) \<longleftrightarrow> A i \<inter> (\<Union>i\<in>I. A i) = {} \<and> disjoint_family_on A I"
+  by (fastforce simp: disjoint_family_on_def)
+
 lemma disjoint_family_on_bisimulation:
   assumes "disjoint_family_on f S"
   and "\<And>n m. n \<in> S \<Longrightarrow> m \<in> S \<Longrightarrow> n \<noteq> m \<Longrightarrow> f n \<inter> f m = {} \<Longrightarrow> g n \<inter> g m = {}"