--- 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
--- 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 = {}"