Just one lemma
authorpaulson <lp15@cam.ac.uk>
Tue, 11 May 2021 15:50:19 +0100
changeset 73927 edb01b64dc16
parent 73926 4121fc47432b
child 73930 0d79ac2eb106
Just one lemma
src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue May 11 14:04:36 2021 +0200
+++ b/src/HOL/Set.thy	Tue May 11 15:50:19 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