# HG changeset patch
# User desharna
# Date 1685700857 -7200
# Node ID 177dae28697b66d0e15e3f7f7666706347831b1f
# Parent  1cadc477f644c89c0fae513f51ff81f4af684c1d
added lemma ffUnion_fsubset_iff

diff -r 1cadc477f644 -r 177dae28697b NEWS
--- a/NEWS	Thu Jun 01 12:08:33 2023 +0100
+++ b/NEWS	Fri Jun 02 12:14:17 2023 +0200
@@ -237,6 +237,7 @@
       fmember_iff_member_fset
       notin_fset
   - Added lemmas.
+      ffUnion_fsubset_iff
       fimage_strict_mono
       wfP_pfsubset
 
diff -r 1cadc477f644 -r 177dae28697b src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Thu Jun 01 12:08:33 2023 +0100
+++ b/src/HOL/Library/FSet.thy	Fri Jun 02 12:14:17 2023 +0200
@@ -1543,6 +1543,12 @@
   done
 
 
+subsection \<open>Lemmas depending on induction\<close>
+
+lemma ffUnion_fsubset_iff: "ffUnion A |\<subseteq>| B \<longleftrightarrow> fBall A (\<lambda>x. x |\<subseteq>| B)"
+  by (induction A) simp_all
+
+
 subsection \<open>Setup for Lifting/Transfer\<close>
 
 subsubsection \<open>Relator and predicator properties\<close>