Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added lemma ffUnion_fsubset_iff
authordesharna
Fri, 02 Jun 2023 12:14:17 +0200
changeset 78132 177dae28697b
parent 78131 1cadc477f644
child 78133 0a098088745b
added lemma ffUnion_fsubset_iff
NEWS file | annotate | diff | comparison | revisions
src/HOL/Library/FSet.thy file | annotate | diff | comparison | revisions 
--- 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
 
--- 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>
isabelle