merged
authorpaulson
Tue, 11 May 2021 18:56:33 +0100
changeset 73930 0d79ac2eb106
parent 73929 70d3c7009a65 (current diff)
parent 73927 edb01b64dc16 (diff)
child 73931 78929c029785
child 73933 51429b78aadf
merged
--- a/src/HOL/Set.thy	Tue May 11 16:55:42 2021 +0200
+++ b/src/HOL/Set.thy	Tue May 11 18:56:33 2021 +0100
@@ -1741,6 +1741,9 @@
 lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
   by blast
 
+lemma subset_vimage_iff: "A \<subseteq> f -` B \<longleftrightarrow> (\<forall>x\<in>A. f x \<in> B)"
+  by auto
+
 lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
   by auto