--- a/src/HOL/Complete_Lattices.thy Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Complete_Lattices.thy Mon Feb 19 16:44:45 2018 +0000
@@ -1099,6 +1099,9 @@
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+lemma disjoint_UN_iff: "disjnt A (\<Union>i\<in>I. B i) \<longleftrightarrow> (\<forall>i\<in>I. disjnt A (B i))"
+ by (auto simp: disjnt_def)
+
lemma UNION_eq: "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
by (auto intro!: SUP_eqI)
@@ -1158,6 +1161,9 @@
lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
by (fact SUP_constant)
+lemma UNION_singleton_eq_range: "(\<Union>x\<in>A. {f x}) = f ` A"
+ by blast
+
lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
by blast