src/HOL/Set.thy
changeset 26150 f6bd8686b71e
parent 25965 05df64f786a4
child 26339 7825c83c9eff
equal deleted inserted replaced
26149:6094349a4de9 26150:f6bd8686b71e
   643   by (simp add: Ball_def)
   643   by (simp add: Ball_def)
   644 
   644 
   645 lemma bex_UNIV [simp]: "Bex UNIV P = Ex P"
   645 lemma bex_UNIV [simp]: "Bex UNIV P = Ex P"
   646   by (simp add: Bex_def)
   646   by (simp add: Bex_def)
   647 
   647 
       
   648 lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A"
       
   649   by auto
       
   650 
   648 
   651 
   649 subsubsection {* The empty set *}
   652 subsubsection {* The empty set *}
   650 
   653 
   651 lemma empty_iff [simp]: "(c : {}) = False"
   654 lemma empty_iff [simp]: "(c : {}) = False"
   652   by (simp add: empty_def)
   655   by (simp add: empty_def)
   949   "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P"
   952   "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P"
   950   -- {* The eta-expansion gives variable-name preservation. *}
   953   -- {* The eta-expansion gives variable-name preservation. *}
   951   by (unfold image_def) blast
   954   by (unfold image_def) blast
   952 
   955 
   953 lemma image_Un: "f`(A Un B) = f`A Un f`B"
   956 lemma image_Un: "f`(A Un B) = f`A Un f`B"
       
   957   by blast
       
   958 
       
   959 lemma image_eq_UN: "f`A = (UN x:A. {f x})"
   954   by blast
   960   by blast
   955 
   961 
   956 lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
   962 lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
   957   by blast
   963   by blast
   958 
   964 
  2107   by blast
  2113   by blast
  2108 
  2114 
  2109 lemma vimage_mono: "A \<subseteq> B ==> f -` A \<subseteq> f -` B"
  2115 lemma vimage_mono: "A \<subseteq> B ==> f -` A \<subseteq> f -` B"
  2110   -- {* monotonicity *}
  2116   -- {* monotonicity *}
  2111   by blast
  2117   by blast
       
  2118 
       
  2119 lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
       
  2120 by (blast intro: sym)
       
  2121 
       
  2122 lemma image_vimage_subset: "f ` (f -` A) <= A"
       
  2123 by blast
       
  2124 
       
  2125 lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
       
  2126 by blast
       
  2127 
       
  2128 lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
       
  2129 by blast
       
  2130 
       
  2131 lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
       
  2132 by blast
       
  2133 
       
  2134 lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"
       
  2135 by blast
  2112 
  2136 
  2113 
  2137 
  2114 subsection {* Getting the Contents of a Singleton Set *}
  2138 subsection {* Getting the Contents of a Singleton Set *}
  2115 
  2139 
  2116 definition
  2140 definition